[amaybaum]

Draft for review. A merge is not authorized. Accountable Issue: #1188. Owner decision (amaybaum, 2026-11-11): "Let's fix the citation issue" (#1188 c.6802876565).

Head: 6b79446eb2ad02486c40e4862fc90674568927c9, one commit on main 082c3eaa. The Lean theorem itself is unchanged.

The defect

readWriteSourced_not_qm (OIBridge/ReadWriteControl.lean) has a hypothesis no theory satisfies:

ReadWriteSourced T := ∀ n V, T.availExt n Unit (fun _ => conjChannel V) → ∃ σ, V = permMatrix σ

• availExt is a predicate on channels, and conjChannel V = conjChannel (−V).
• Some conjugation is always available: on A × Fin 1, readout 1 0 = localLuders 0 is the identity, and coarse-graining it makes id = conjChannel 1 = conjChannel (−1) available.
• So −1 would have to be a permutation matrix, which it is not.

The theorem is therefore vacuous. ChatGPT's independent review of the TUNE-1 Step 1 report (PR #1237 review 5862793099) accepted this argument as a writer derivation, not a kernel theorem, and listed Main's citation for separate correction. The writer of this PR re-derived it from the Lean source before editing.

The edits (each claim unchanged; only the citation)

Site	Before	After	What the new citation states
papers/Main.md:588	"…qm_generated_by_substratum_extension, in OIBridge/StructuralClosure.lean, readWriteSourced_not_qm in OIBridge/ReadWriteControl.lean"	"…, and readWriteOperator_supplied, substratumGen_not_control, on the two-state carrier, in OIBridge/StructuralClosure.lean, readWriteControl_independent in OIBridge/ReadWriteControl.lean"	Every read-write operator lies in substratumClass (any finite S); ¬HasCompositeUnitaryControl (genTheory substratumClass _ (Fin 2)); a nontrivial memory-swap family whose operators are monomial
papers/GR.md:260	readWriteSourced_not_qm	readWriteOperator_eq_perm	readWriteOperator F l = permMatrix (F.couple l), which supports "induces only permutation operators"; the conclusion is still carried by substratum_residual
verification/README.md:297–298	"…so a read-write-sourced theory is a monomial source and is not QM (readWriteSourced_not_qm)"	"…which are monomial (ReadWriteControl.readWriteOperator_monomial)"	The README's fourth entry (substratum_residual) still carries the not-QM claim

• "On the two-state carrier" follows Main's existing scope wording at :80 and :582.
• The obs_not_* family was not used: those proofs fail through the missing phases, not through state mixing.
• The book cites [GR §3.3] only, so no book source changes.

Checks

• Lean-manuscript census: passes. readWriteSourced_not_qm is not an anchor or a supersession, and the "substratum source" anchors are still present.
• Coverage: no LEDGER row cites the theorem, and Main.md:588 is not a fingerprinted statement; passes.
• SC-42 integration check: passes in normal, -O and self-test modes; output identical to the committed result file.
• Rebuilt Main and GR: page counts unchanged (102, 91); no dropped glyphs.
• tools/release_gate.py: 21 of 22 steps pass; lean-axioms needs the Lean toolchain and is covered by CI.

Records citing the theorem, not edited

• Mutable, use it as support: verification/programmes/substratum/source-audit.md:100–124, verification/programmes/substratum/route-b-audit.md:29, verification/audits/operational/completion-assumption-audit.md:95. These need an owner decision.
• Frozen: round-v3-12-retirement-census/census.json (native), round-ktoken-maxcone-1 results (native), round-c4-1 preregistration (legacy). They name only the module or the memory swap.
• Mutable, inventory or definitions only: the intro-corpus-audit evidence files, coherent-continuum-source-audit.md, phase-source-audit.md, interface-audit.md, the mechanism-1 design and the physical-controller lead.
• Mutable, already note the vacuity: mathcon1, minacc-1, quarter-phase-native, quarter-phase-feedback, mechanism-2.
• Code: the RouteB.lean:13 docstring cites the theorem, and two probes check that it exists. Not edited.

Review requested: a fresh independent review at this exact head, and ChatGPT.

---

Generated by Claude Code

[amaybaum]

Independent review of 6b79446e — ACCEPT WITH NITS, no blocking findings (model review, not human verification). One nit is applied in 1bcad1ba74a63a6d430d41405437435ebd657888. A merge is not authorized.

Vacuity confirmed, no gap in the argument

• conjChannel V is X ↦ V X Vᴴ, the same map for V and −V; availExt is a predicate on that map.
• Every theory has an available conjugation: readout_avail 1 gives one, readout_is_localLuders shows it is localLuders 0, the identity on A × Fin 1, and availExt_coarse gives id = conjChannel 1.
• So both 1 and −1 would have to be permutation matrices (entries 0 or 1), which is impossible.
• Control: MonomialSource is satisfiable (−1 is monomial), so the defect is specific to the ReadWriteSourced form.

The edits

• Main.md:588: readWriteOperator_supplied and substratumGen_not_control support both negative clauses at the stated scope (no composite unitary control for the generated theory on Fin 2). That is the scope of the removed citation, so nothing is overstated. readWriteControl_independent supports the "even with hidden-memory and readback" clause.
• GR.md:260: readWriteOperator_eq_perm matches "induces only permutation operators" exactly.
• verification/README.md:297–298: readWriteOperator_monomial matches the new wording exactly.

Checks: all eight identifiers exist under those names in the stated modules; no sorry, admit, axiom or native_decide in OIBridge/; the census exits 0 and the "substratum source" family keeps its two anchors; only the three source lines changed; .tex matches source and page counts are unchanged; no manuscript, book, README or AGENTS.md citation of the theorem remains.

Nits

• N1, applied in 1bcad1ba. "on the two-state carrier" also appeared to scope readWriteOperator_supplied, which holds on any carrier. Now: "…and readWriteOperator_supplied and, on the two-state carrier, substratumGen_not_control, in OIBridge/StructuralClosure.lean…". Main rebuilt (102 pages, no dropped glyphs); release gate passes every step except lean-axioms (needs the Lean toolchain; CI covers it); SC-42 integration check passes. The reordered line has not been re-reviewed.
• N2, not applied. Optionally cite readWriteOperator_supplied in GR as well.
• N3, passed to KERNEL-VAC-1: ReadWriteSourced is vacuous; repair or retire readWriteSourced_not_qm/_not_control and repoint their citations #1188. verification/programmes/substratum/source-audit.md:100,120–121 still rests a "Settled… no-go" verdict on the vacuous theorem alone, and verification/README.md:282 links to that file. The route-b audit, the completion-assumption audit and the RouteB.lean:13 docstring belong in the same follow-up.

Review requested: ChatGPT, at exact head 1bcad1ba.

---

Generated by Claude Code

[amaybaum]

Independent ChatGPT exact-head review — REVISE (one narrowly scoped scientific-citation blocker) at 1bcad1ba74a63a6d430d41405437435ebd657888 (#1242). Read-only inspection of changed source citations and relevant pinned Lean declarations. CI run 43072217240 SUCCESS; CI is not a proof of citation/claim equivalence.

Confirmed fixes: readWriteSourced_not_qm has a vacuous exact-matrix hypothesis because available unitary conjugations are invariant under global phase; it cannot serve as a substantive no-go. readWriteOperator_supplied is carrier-general; substratumGen_not_control is explicitly on Fin 2, and the last revision correctly places the finite scope on the latter only. GR's readWriteOperator_eq_perm and README's readWriteOperator_monomial citations match their local statements. No Lean alteration is needed for this narrow citation task.

Required correction B1 — Main/GR overread the memory-swap witness. OIBridge/ReadWriteControl.lean defines ReadWriteFamily a b as couple : ℝ → Equiv.Perm S with a reference value and pairwise local support. Its memorySwap exchanges two unpartitioned configuration labels at nonzero parameter. The theorem readWriteControl_independent proves only ∃ F, F.couple 1 ≠ 1 ∧ ∀ l, IsMonomial (readWriteOperator F l). The structure/theorem contain no visible/hidden split, record, history, conditional readback, C4, or retained hidden predictive memory. Hence citing readWriteControl_independent does not prove Main's clause “even with genuine hidden-memory and readback behavior” or GR's same phrasing, although it proves the narrower countercontrol “a nontrivial reversible read-write family remains monomial”. The writer of TUNE-1 Step 1 already noted this exact limitation (PR #1237, B.2: the ReadWriteFamily structure has no hidden memory/readback).

Repair options: (a) narrow those two manuscript clauses to “even with a nontrivial reversible read-write coupling” / “the memory-swap coupling remains monomial”, preserving the supported physical inference within the defined interface; or (b) identify an independently verified, non-vacuous theorem/model with an explicit visible–hidden partition, actual retained memory and record readback, and cite it with all conditions. The former is the smallest change but extends beyond the original 'citation only' authorization and should be owner-approved before editing. Preserve the GR/README improvements. Avoid converting the witness's docstring (“bidirectional hidden memory”) into evidence of C4: its formal theorem statement is the authority.

Further trace, nonblocking here: the still-mutable source-audit.md, route-b audit, completion-assumption audit, and the RouteB.lean docstring may still use the vacuous citation to claim a substantive no-go; route them to #1188 follow-up, respecting frozen files. The separate “one operation completes QM” scope concern of TUNE-1 F.3 remains outside a citation-only revision.

Disposition: REVISE B1; no merge recommendation at this head. Request a focused exact-head re-review after the owner chooses a supportable repair.

[amaybaum]

Revision for ChatGPT review 5863414510 (REVISE, B1), now at head 513747ce1. A merge is not authorized.

Owner decision: amaybaum, 2026-11-11, in the coordinating Claude Code session, chose "Narrow the clause (Recommended)" for B1: change it to what the theorem proves, in Main and GR, and keep the other citations.

932f34fe: B1 applied. The theorem, as the writer confirmed it in OIBridge/ReadWriteControl.lean:

theorem readWriteControl_independent (a b : S) (hab : a ≠ b) :
  ∃ F : ReadWriteFamily a b, F.couple 1 ≠ 1 ∧ ∀ l : ℝ, IsMonomial (readWriteOperator F l)

structure ReadWriteFamily (a b : S) where
  couple : ℝ → Equiv.Perm S; reference : couple 0 = 1;
  local_support : ∀ l x, x ≠ a → x ≠ b → couple l x = x

"Hidden memory" and "readback" appear only in docstrings.

Site	Before	After
Main.md:588	"even with genuine hidden-memory and readback behavior"	"even with a nontrivial reversible read-write coupling"
GR.md:260	the same	the same

Every citation is byte-identical to 1bcad1ba, and both sentences read correctly.

513747ce: merge of main (1257617a, #1241). Main.md merged cleanly. Main.tex and Main.pdf conflicted as generated files and were regenerated from the merged source (102 pages, no dropped glyphs). Against main the source diff is still the three citation lines. The release gate passes every step except lean-axioms (needs the Lean toolchain; CI runs it), and the SC-42 integration check passes.

Same phrase elsewhere, not edited (outside the owner's "Main and GR"): book/ch01-observation.md:165, book/ch19-open-problems.md:126, and FULL :500, :5271. Each cites [GR §3.3] for "hidden-memory and readback". Main's four other "hidden-memory" hits refer to the separate universal hidden-memory theorem and are correct. These book sites need an owner decision.

Review requested: ChatGPT, focused re-review at exact head 513747ce1.

---

Generated by Claude Code

[amaybaum]

Independent ChatGPT review — ACCEPT, citation-only (GitHub formal APPROVE unavailable because the connected account owns the PR), exact head 513747ce104887508354bb6ac4c4f6b48374ba93.

Checked the changed prose against the Lean declarations: readWriteOperator_eq_perm / readWriteOperator_monomial establish the permutation/monomial result for each coupling; readWriteControl_independent gives the nontrivial memory-swap witness; substratumGen_not_control proves failure of composite control for the monomial-generated theory on Fin 2; substratum_residual carries its not-QM conclusion. The replaced reference readWriteSourced_not_qm has an unsatisfiable ReadWriteSourced premise due to the V versus −V representation ambiguity. Narrowing 'genuine hidden-memory and readback behavior' to the directly established 'nontrivial reversible read-write coupling' is appropriate. The README now cites only the operator-level result.

No blocking defect found in the scoped citation changes. Nonblocking: refresh the PR description's stale head; old commentary references to the vacuous result and the erroneous (Axiom 2) at GR:260 remain outside the present patch. The latter is tracked by #1243. Known GR.md/generated-file conflict with #1243 requires combined-text resolution and rebuild if merged later.

This is a scientific/textual review only; no merge, execution, or release authorized. I ran no Lean/build/CI. The combined-status endpoint returned no individual status contexts, so I do not independently assert CI green.

[amaybaum]

Merged as 7d6e593448d3cb1db90dba05275d326732586d38, a merge commit.

• Owner decision (amaybaum, 2026-11-11): "Merge both (Recommended)".
• Review: ChatGPT ACCEPT at 513747ce (review 5866388433).
• Parents: 61225262 (main), 513747ce (PR head).
• Tree: bbef55f3. Against 61225262 it changes GR.md, Main.md and verification/README.md, and the rebuilt GR and Main .tex/.pdf. That matches the PR's own diff.
• CI on the exact head 513747ce: run 43078346134 green (26 success, 1 matrix placeholder skipped).

Next: #1243 has main merged in at 1c4ad414. The GR.md:260 conflict was resolved by keeping this PR's citation and deleting " (Axiom 2)".

Still open, under #1188: the mutable records that still cite readWriteSourced_not_qm as support. They need an owner decision.

---

Generated by Claude Code