[amaybaum]

Tracks #1146.

Authorization

• Owner ruling K1-RDY: paper-only readiness investigation under fixed selection rule #1031 c.6666613671 (amaybaum, 2026-11-05) covers one Main edit PR for repairs R1′–R5 as corrected by the independent review. It is limited to drafting, local checks, a push and a draft PR. It does not authorize merge, dispatch or any Lean change.
• Main: state the operational-completion characterization and cite kernel proofs directly (#1146) #1154 c.6670348300 authorizes the SC-42 pin and anchor update.

Sources

• The audit (MAIN-GR-DEP: audit Main's citations of GR §3.3 used as support (Main upstream-independence) #1146 c.6665824857) and the independent review (MAIN-GR-DEP: audit Main's citations of GR §3.3 used as support (Main upstream-independence) #1146 c.6665830700). Where they differ, the review governs.
• This PR's exact-head review (c.6666966273) and its delta check.

Commits (base / D = f051916a113c9412b3efbb1ff813ec57c2ed265d)

SHA	Content
9f38b2eaa91ee6e0f5f49df6cd3f8598729d5bc6	R1′–R5
5ef3f563ce8571a917714e74744049a6ecc823e0	review fixes
124b0d143658bf90ba68c425ada570735c09ccfb	delta-check note wording; l.590 citation placement
80865f7286d2443c7110ef0fb72199f4d4457c91	merge of main d39defd0bc900e711ae4294ef80d095022703970 (#1153); conflicts below
95ee4995b640ae0b3895ea80e2dd6b702c7669f6	SC-42 pin/anchor update and regenerated outputs
a8c8ed9a8cc03c456ca8d9ba6e72e0d443cc6da3	merge of main 258a0e3e, made by the coordinator via GitHub
22e328dc6699cd55c58a26c659e1389f62859be3	head: Main l.590 word order only, to restore guard R7-PTR's line-start pin

Conflict resolution in the first merge (80865f72)

• papers/Main.md auto-merged. A line-by-line check against both parents confirms that Main: finiteness attribution and section reference (#1015) #1153's ll.38/46/718 and this PR's 20 lines do not overlap.
• papers/Main.tex and papers/Main.pdf conflicted. They were not hand-merged; they were regenerated from the merged Main.md with sh ./build.sh Main.
• sc42-integration-result.json was taken from main, then regenerated in 95ee4995.

Files changed against main: papers/Main.md, papers/Main.tex, papers/Main.pdf, verification/coverage/LEDGER.json, and in verification/audits/manuscript/bell-operational-reconciliation-20261029/: check_sc42_integration.py, sc42-intended-sites.json, sc42-integration-result.json, sc42-integration-controls.json.

All Main edits are in-line. Only these 20 lines change: 82, 99, 147, 216, 218, 274, 354, 356, 358, 556, 564, 584, 586, 590, 600, 644, 646, 654, 712, 776.

Repairs and the findings behind them

Repair	Main line(s)	Edit	Finding
R1′	564	Replaces the [GR §3.3] pointer with kernel citations: the characterization exactAll_iff_physical_general, its necessity physical_of_exactAll, its sufficiency exactAll_of_physical_general, and main_result. Adds the six rules (a)–(f) of FiniteOperationalTheory.	Audit §3 Group A (a)/(b); review 2, 6(b)
R1′	564	Adds one clause per condition (i)–(v), each defining it from its kernel predicate: CompositeOperationalValidity, SystemToLevelOne, InertSpectatorCompositionality, HasCompositeUnitaryControl, IteratedAncillaClosure.	Review 6(a)
R1′	564	"finite Kraus instruments" → "normalized finite Kraus instruments".	Review 6(c)
R1′	564	The independence clause now reads "witnessed on the qubit by theories realizing one fixed finite C1–C4 process" (kernel: five_way_minimality, oi_alone_not_qm).	Audit l.564 scope finding; review 5
R1′	358	[GR §3.3], kernel-verified → §3.4; kernel: exactAll_iff_physical_general, with necessity physical_of_exactAll, sufficiency exactAll_of_physical_general, and main_result.	Review 4 (§A.34 directional witnesses)
R1′	644	([GR §3.3]; Remark below) → (Remark, the operational-extension boundary; Remark below).	Review 6(d)
R1′	82, 99, 216, 218, 354, 356, 556, 584b, 600, 646, 654, 776	Each pointer is retargeted to §3.4 or to the operational-extension-boundary Remark, as in the audit's R1 table.	Audit R1 table
R2	584a	Cites sameData_unitary_or_transpose with its hypotheses: Hermitian menus spanning the full matrix algebra, the unit at a common index, and separating PSD state families generating the positive cone.	Audit Group B; review 3, 7
R3′	274	Drops [GR §3.3]; and keeps the kernel citations.	Audit R3; review 8
R3′	712	([GR §3.3]; §3.4) → (§3.4), and additional structure ([GR §3.3]) → additional structure (§3.2).	Audit R3; review 8
R3′	590	"See [GR §3.3] for the full statement and scope" becomes a scope sentence: the carrier-general OI⁺ has no OI-core clause, and the OI-core clause is defined on the qubit, where it does not change the class (oiPlus_qubit_iff). The l.588 display's directional witnesses qm_of_oiPlus and oiPlus_of_qm are named. The five [GR §3.3]; prefixes are dropped.	Review 5 (NEW l.590 drift), 4 (l.588 witnesses), 8
Review fix	586, 590	l.586: "define … OI⁺ by adding well-formedness together with" → "as well-formedness together with", consistent with l.590's statement that the carrier-general OI⁺ has no OI-core clause. l.590: the independence sentence now reads "Each added principle is independently necessary, on the qubit, relative to the OI core, well-formedness, and the other two (kernel: oiPlus_independence in OIBridge/CompletedOI.lean)". In 22e328dc the qubit scope was placed mid-sentence, a change of word order only, so that the line again starts with the prefix guard R7-PTR pins and edge_rigidity_probe.py stays untouched.	#1154 review c.6666966273, required change 2 and option; delta check; R7-PTR line-start pin
R4	147	(§1.3; [GR §2.2]) → (§1.3).	Audit Group D; review 9
R5	LEDGER	MAIN:T-statement is re-affirmed with fingerprint 9dc06d98eba944bd → 261664b9b3f2b961, computed by tools/proof_census.py. The note is corrected: items (1) and (2) are carried by the equivalence-chain and memory-conditions rows, with the stochastic-inverse lemma; item (3) by the finite-horizon process dilation, the finite operational realization and gluing, and the uniform continuum realization rows. The characterization clause of item (4) is carried by no Main row; its support is the kernel theorems now cited in Main §3.4.	Review 11(a); owner chose correcting the note; #1154 review required change 1; delta-check wording
R5	Main.tex/.pdf	Regenerated with sh ./build.sh Main.	Review 11(b); §A.25 step 5
SC-42	checker, site table, outputs	The three Main pins in check_sc42_integration.py follow the edited sentences: ([GR §3.3]; Remark below) → (Remark, the operational-extension boundary; Remark below); (§3.4; [GR §3.3]) → (§3.4); characterization ([GR §3.3]) takes → characterization of §3.4 takes. The site-table anchor for l.586 changes from by adding well-formedness to as well-formedness . Both outputs are regenerated on the merged base.	CI core B failure at 124b0d14; owner authorization #1154 c.6670348300

SC-42

• Regenerated in 95ee4995 on main d39defd0 plus this branch: verdict PASS (664 checks, no failed predicates), and all 9 controls pass.
• Against main's committed outputs, the only differences are checker_sha256 (26966c7d… → 6573db27…), site_table_sha256 (77b5ba19… → eb0b5866…) and the label of the one pin at l.218.
• At head 22e328dc, both outputs replay byte for byte with no regeneration.

Re-grep. \[GR § in papers/Main.md: 0 (was 26). All 5 "SM/GR" mentions survive.

Census (§A.35). No registry change was made.

Kernel identifiers cited (each read at base before citing)

Identifier	Location
exactAll_iff_physical_general	GeneralCarrier.lean:100
exactAll_of_physical_general	GeneralCarrier.lean:93
main_result	GeneralCarrier.lean:188
oi_alone_not_qm	GeneralCarrier.lean:160
physical_of_exactAll	PhysicalCharacterization.lean:301
five_way_minimality	RankGapTheory.lean:702
FiniteOperationalTheory	OperationalAssembly.lean:594
readout_is_localLuders	OperationalAssembly.lean
HasCompositeUnitaryControl	OperationalAssembly.lean:665
CompositeOperationalValidity	OperationalValidity.lean:88
SystemToLevelOne	LevelOneSeam.lean:117
InertSpectatorCompositionality	SpectatorBridge.lean:223
IteratedAncillaClosure	AncillaClosure.lean:247
sameData_unitary_or_transpose	JordanClassification.lean:1109
carrier_general_oiPlus	CarrierGeneralOIPlus.lean:213
qm_of_oiPlus	CarrierGeneralOIPlus.lean:191
oiPlus_of_qm	CarrierGeneralOIPlus.lean:198
oiPlus_qubit_iff	CarrierGeneralOIPlus.lean:224
oiPlus_independence	CompletedOI.lean:506 (the version relative to the OI core)

Checks (local, at head 22e328dc)

Check	rc
edge_rigidity_probe (as in Core probes B)	0 (91 PASS, 0 FAIL)
SC-42 normal / -O (result replays byte for byte)	0 / 0
SC-42 self-test / -O (controls replay byte for byte)	0 / 0
proof_census	0
coverage_check	0
lean_manuscript_census	0
staleness_check	0
voice_check	0
claims_check	0
duplicate_check	0
architecture_check	0

• proof_census reports 130 statements with the same IDs. The only fingerprint that moves against main is MAIN:T-statement (261664b9b3f2b961).
• build.sh Main reports OK at 101 pages, with no dropped glyphs.
• Earlier heads also passed dependency_label --strict, mirror, citation, legacy_records, artifact_placement and toolchain.
• Lean was not built locally (§A.40), and no Lean file changed.

Follow-ups (not in this PR)

1. Downstream GR pointer correction (owner: track as follow-up). GR §3.3's characterization paragraph should add [Main §3.4] beside its kernel pointers. Downstream papers and book mirrors that cite GR §3.3 for the characterization may retarget to [Main §3.4] (review 13 gives counts). A chapter and FULL.md move together.
2. Root-graph question for ll.586–590. It is open whether any l.82 root consumes the OI⁺, typed, quasilocal and layer-flow material, which decides whether that material should be relocated (audit §3 C(i); review 14).
3. Unnamed downstream references at l.72 and l.99 ("companion work", "companions") need a separate scoped check (review 12).
4. A1–A6 dependency on [Substratum §3.1] in the substratum-source and layer-flow forms is a separate independence question (audit §3 C(ii)).

Status: Main l.590 word order changed at 22e328d (R7-PTR line-start pin; word order only); SC-42 pin/anchor update authorized at c.6670348300; independent review pending; merge not authorized

🤖 Generated with Claude Code

https://claude.ai/code/session_011zDyUSyEszk3JJx83uXKKq

[amaybaum]

Independent exact-head review at 9f38b2ea: ACCEPT WITH CHANGES (two one-sentence fixes)

The review was read-only, with no Lean build.

Confirmed

1. l.564 matches the Lean definitions with no strengthening.
   • Rules (a)–(f) match the fields of FiniteOperationalTheory (OperationalAssembly.lean:594–653).
   • Conditions (i)–(v) match CompositeOperationalValidity (OperationalValidity.lean:88), SystemToLevelOne (LevelOneSeam.lean:117), InertSpectatorCompositionality (SpectatorBridge.lean:223, IsSpectatorExtension :180), HasCompositeUnitaryControl and IteratedAncillaClosure (AncillaClosure.lean:247).
   • "Normalized" is correct: the Kraus operators sum to the identity.
   • The qubit wording is accurate: RealizesSealedOICore is defined only on the qubit.
2. Writer's deviations: all fine.
   • (a) Rule (e) states the action on X⊗Y, and readout_is_localLuders gives the form on every matrix. That is exactly what the kernel says, and architecture_check reports 0 violations.
   • (b) The OI⁺ file attributions pick the right module each time. oiPlus_independence comes from CompletedOI.lean:506, which includes the OI core. qm_of_oiPlus/oiPlus_of_qm come from CarrierGeneralOIPlus.lean:191/198, the carrier-general versions. oiPlus_qubit_iff is at :224.
   • (c) Citing five_way_minimality/oi_alone_not_qm at the independence clause alone is adequate.
   • (d) Accepted in substance, but needs the wording fix below.
3. §A.34 directions. l.358 names necessity physical_of_exactAll and sufficiency exactAll_of_physical_general. l.588 names qm_of_oiPlus/oiPlus_of_qm. The l.590 scope sentence matches the kernel.
4. LEDGER fingerprint. proof_census recomputed on both trees: 130 statements, the same IDs. The only change is MAIN:T-statement, 9dc06d98eba944bd → 261664b9b3f2b961. The item (4) wording claims no Main row and names the kernel theorem with both directions.
5. Scope. Zero [GR § remain, and all five "SM/GR" mentions survive. There are exactly 19 hunks. ll.38/46/718 are untouched. "Remark below" is kept at l.644.
6. Generated files. Main.tex reproduces byte-for-byte, and the stamp matches. Main.pdf is 101 pages with no missing glyphs. staleness, lean_manuscript_census, voice, dependency_label --strict, claims, duplicate, citation and mirror all pass. architecture_check exits 1 locally on "record-fibre controls unavailable", and the base commit fails the same way, so this comes from the environment, not the PR.
7. Register: clean.

Required changes

1. LEDGER.json MAIN:T-statement note. No "finite-realization" rows exist. Replace "Items (1) to (3) are carried by the equivalence-chain, memory-condition and finite-realization rows." with:

   Items (1) to (3) are carried by the equivalence-chain and memory-conditions rows, with the stochastic-inverse lemma; item (3) by the finite-horizon process dilation, the finite operational realization and gluing, and the uniform continuum realization rows.

2. Main.md l.586. "define quantum-complete OI (OI⁺) by adding well-formedness together with" reads as the OI core plus additions, which the new l.590 denies on a general carrier (§A.30). Change "by adding well-formedness together with" → "as well-formedness together with". l.586 is not fingerprinted.
   • Optional: move "on the qubit" into the sentence "Each added principle is independently necessary…".

After these two changes, regenerate Main.tex/pdf and confirm with proof_census that no fingerprint moves. Merge is a separate owner decision, and integration is serialized after #1153.

---

Generated by Claude Code

[amaybaum]

Delta check 9f38b2ea → 5ef3f563: ACCEPT

1. l.586 now reads "define quantum-complete OI (OI⁺) as well-formedness together with …". This agrees with l.590 and with the carrier-general OIPlus definition (CarrierGeneralOIPlus.lean:185).

2. l.590 keeps its qubit scope: "On the qubit, each added principle is independently necessary relative to the OI core, well-formedness, and the other two". The dropped clause only repeated that scope. oiPlus_independence is still cited from CompletedOI.lean:506, the qubit statement with the OI core.

   • Optional: move that citation to just after the "On the qubit" sentence.

3. Ledger note. The four row ids exist: MAIN:L-stochastic-inverse, MAIN:T-finite-horizon-process-dilation, MAIN:T-finite-operational-realization-gluing-form and MAIN:T-uniform-continuum-realization-mutual-density.

   • The stored line fields of the last three were already 6 behind at the base. No gate reads those fields, and this PR did not cause the drift.

4. Note wording ruling. The prescribed sentence named item (3) twice, so the writer's proposal is adopted:

   Items (1) and (2) are carried by the equivalence-chain and memory-conditions rows, with the stochastic-inverse lemma; item (3) by the finite-horizon process dilation, the finite operational realization and gluing, and the uniform continuum realization rows.

   Notes are not fingerprinted, so nothing needs to be regenerated.

5. Fingerprints. 130 statement ids. The only fingerprint that changed is MAIN:T-statement (9dc06d98eba944bd → 261664b9b3f2b961).

6. Build. Main.tex reproduces byte-for-byte from source, and the stamp matches Main.md. Main.pdf has 101 pages and contains no "GR §". staleness, census and voice checks pass.

7. Scope. The diff is 20 single-line changes: the 19 earlier lines plus l.586. ll.38/46/718 are untouched, and there is no register issue.

Next: apply the item 4 wording, check it, integrate with main after #1153, and run exact-head CI. Merge is a separate owner decision.

---

Generated by Claude Code

[amaybaum]

124b0d14: coordinator mechanical check.

• The commit has one parent, 5ef3f563. It changes Main.md (l.590 only), Main.tex, Main.pdf and LEDGER.json (the MAIN:T-statement note only).
• The note now reads "Items (1) and (2) …; item (3) by …", the wording adopted in the delta check.
• In l.590, the oiPlus_independence citation (OIBridge/CompletedOI.lean) moved within the line. It now follows "On the qubit, each added principle is independently necessary…", and the scope sentence keeps its CarrierGeneralOIPlus citations. No wording or claim changed.
• The writer reports these checks:
  • proof_census: 130 statement ids, and no fingerprint moved (MAIN:T-statement stays 261664b9b3f2b961);
  • coverage, census, staleness and architecture checks pass;
  • the Main.pdf rebuild is 101 pages.

Next: integrate with main after #1153, then exact-head CI. Merge is a separate owner decision.

---

Generated by Claude Code

[amaybaum]

Owner decision: SC-42 checker pins and site-table anchor. amaybaum, Claude Code session (question dialog), 2026-11-05, about 21:00Z. The owner chose "Authorize, with review":

Apply the 4-line pin/anchor update after #1153 lands, regenerate on that base. Independent review must confirm each new pin guards the same scope as the old one (no weakened guard). Then CI and your separate merge decision.

Context. At 124b0d14 the SC-42 integration checker returns FAIL, not only a mismatch with the committed outputs. Five predicates flip:

• the l.586 site-table anchor, which contains "by adding well-formedness" (two predicates);
• the three checker PINS that quote the old [GR §3.3] text at ll.218, 644 and 654.

Each of these follows from edits this PR made deliberately.

The update (precedent: #1140, 6a019d1b). It changes four lines:

• check_sc42_integration.py PINS:
  • "([GR §3.3]; Remark below)" → "(Remark, the operational-extension boundary; Remark below)";
  • "(§3.4; [GR §3.3])" → "(§3.4)";
  • "characterization ([GR §3.3]) takes" → "characterization of §3.4 takes".
• sc42-intended-sites.json anchor: "by adding well-formedness " → "as well-formedness ".

The committed result and controls are then regenerated on the base that includes #1153.

---

Generated by Claude Code

[amaybaum]

Independent review: integration 80865f72 and SC-42 pin update 95ee4995 — ACCEPT

This is the review that ruling c.6670348300 requires. It was read-only and ran in a scratch extraction.

0. 124b0d14.

   • The ledger note has the ruled wording.
   • The oiPlus_independence citation (CompletedOI.lean, core-including qubit theorem) moved to directly after "On the qubit, each added principle…".
   • Nothing else changed.

1. Merge.

   • git merge-tree 124b0d14 d39defd0 merges Main.md and LEDGER.json cleanly and is identical to 80865f72. Every merged line comes from the side that changed it. Main: finiteness attribution and section reference (#1015) #1153's ll.38/46/718 are preserved.
   • Only Main.tex and Main.pdf conflicted. Both were regenerated: Main.tex reproduces byte-for-byte, its stamp equals sha256(Main.md), and Main.pdf is 101 pages.

2. The new pins guard the same scope, with no weakened guard. The checker requires each pin to occur exactly once (l.247) and the anchor to match exactly one line (ll.219–222).

   Pin	Old	New	Only change
   l.644	once	once	[GR §3.3] → Remark, the operational-extension boundary
   l.654	once	once	; [GR §3.3] deleted
   l.218	once	once	([GR §3.3]) → of §3.4

   • Every other word is unchanged, so the "exactly when / exactly under / characterized by the five conditions" claims and their kinematics scope are still pinned verbatim.
   • The l.586 anchor matches exactly the same paragraph, with mention count 1. The old anchor would have matched nothing.
   • No count, predicate or control was edited.

3. Regenerated outputs.

   • The normal run, -O, --self-test and -O --self-test all exit 0 and are byte-identical to the committed result and controls.
   • The verdict is PASS: 664 checks, 0 failed.
   • All 9 controls pass: the unchanged source exits 0, and each of the 8 must-fail variants exits 1.
   • Against main, only checker_sha256, site_table_sha256 and the l.218 predicate label differ.

4. Fingerprints. 130 statement ids. The only moved fingerprint is MAIN:T-statement (9dc06d98eba944bd → 261664b9b3f2b961), and coverage_check is OK.

5. Correction to the earlier Main: state the operational-completion characterization and cite kernel proofs directly (#1146) #1154 reviews.

   • The architecture_check exit 1 reported there was not environmental. Earlier git archive extractions dropped paths that .gitattributes excludes from git archive.
   • With the full tree present, it passes: 0 violations, record-fibre controls PASS.

6. CI at 95ee4995. Still running when checked, with no failures.

Merge requires green exact-head CI and is a separate owner decision.

---

Generated by Claude Code

[amaybaum]

a8c8ed9a → 22e328dc: word order changed at Main l.590 to satisfy guard R7-PTR. This edit falls under the existing ruling #1031 c.6666613671. No guard was edited.

Background.

• a8c8ed9a merges main 258a0e3e into this branch. Its net diff is identical to the reviewed 95ee4995.
• CI at a8c8ed9a failed in "Core probes B": edge_rigidity_probe.py reported 1 FAIL out of 91 checks, from guard R7-PTR (probe ll.3127–3192).
• R7-PTR requires exactly one Main line that begins Each added principle is independently necessary and names nine kernel identifiers.
• The optional review move at 5ef3f563 made l.590 begin "On the qubit, …", so no line matched any more. All nine names were still present.
• The guard is not part of any frozen record: it is not listed in legacy-records.json and sits outside every round's record directory.

Change. In Main l.590:

• before: "On the qubit, each added principle is independently necessary relative to …"
• after: "Each added principle is independently necessary, on the qubit, relative to …"

Main.tex and Main.pdf were regenerated. The coordinator checked mechanically that the word-diff shows exactly this reordering and nothing else, and that the qubit scope is kept.

Writer-reported checks at 22e328dc:

• the probe gives 91 PASS / 0 FAIL;
• SC-42 replays the committed result and controls byte-for-byte, with no regeneration needed;
• proof_census shows no fingerprint moved;
• coverage, census, staleness, voice, claims, duplicate and architecture all return rc 0.

Exact-head CI is running. Merge is a separate owner decision.

---

Generated by Claude Code

[amaybaum]

Merge record. This PR was merged under owner approval #1031 c.6676219154.

• Pre-merge checks. Immediately before merging, the head and base were checked again:
  • head 22e328dc6699cd55c58a26c659e1389f62859be3;
  • base = main 258a0e3e;
  • mergeable state clean;
  • exact-head CI green (25 success, 1 skipped).
• Merge. It was merged as a normal merge commit with expectedHeadSha: 92f4f2702a75c596b6b467370a6acdfbd3d6db7a. Its parents are 258a0e3e and 22e328dc, so merge ancestry is preserved.
• Post-merge main CI at 92f4f270: green (26 success, 1 skipped).
• Main citations. The [GR § citations in papers/Main.md go from 26 to 0.
• MAIN:T-statement fingerprint: 9dc06d98eba944bd → 261664b9b3f2b961. This is the only fingerprint that changed.

---

Generated by Claude Code