[amaybaum]

Status: DRAFT — author checkpoint, not independently accepted or merge-ready

Head at filing: 83b00491168e17f26f409c1d4ada11da99453ce6; compare exact current head before reviewing.

• In Substratum §4, replace the false semigroup-transfer argument with the existing Lean-proved fixed-carrier block-word proposition, separately citing both Lean directions. Keep completeness of the four generator families open.
• Restore sound independent observations (scoped time reversal, global phase, graph and alphabet cases), and change direct Theorem 23 and synthesis references from the refuted lemma to an explicit open assumption.
• Anchor WordTraceSufficiency and SemigroupTransfer families in verification/lean-manuscript-census.json; retain writer handoff under tracks/SC44-lemma-24-1/README.md.
• New direct blocker: SC-45 #979 found that Theorem 24(i)'s arbitrary state relabelling does not preserve transitions at a fixed observer partition. That soundness issue has its own unit and is not silently included as an accepted fix in this PR.
• Still required: independent review of this exact head, review of the old Lemma 24.1 identifier's retirement, coverage+census+release gates, regenerated .tex and PDF, direct and downstream corpus corrections, and cross-unit reconciliation. No Lean changes or fresh axiom results are claimed. No merge is authorized.

[amaybaum]

The writer prepared a separate reconciliation preview with SC-45 #981: #982 at 053130e6, stacked on this PR. It retains this branch's Lean-proved Proposition 24.2 and the retired old Lemma 24.1, but replaces the unsupported full-observable generator language with SC-45's fixed-interface theorem and narrows immediate dependent claims. This is not acceptance of SC-44 or an authorization to merge; original correction and independent review remain separate. See #946 gate and preview README.

[amaybaum]

Independent scientific review — REVISE (owner-relayed, exact head 87d0b03f4affe1d5da0b8d5c11ee76a4d0f6d0d7)

Provenance: This records the owner's report of the outside review, not an additional independent review by this writer. The full reviewer-authored line-by-line replacement text was not supplied in this chat and is not present in this PR's discussion; this comment is a faithful summary, not a claim that it reproduces those replacements verbatim.

Proved result to preserve. Fixed-carrier block-word trace rigidity with full block spanning is established by the cited Lean theorems WT2gen_oneSided, WT3_spanning_iff, blockSpanning_of_wordTracesEqual, and trace_wordEval_hiddenConjugate. It does not supply full generator completeness without a map from selected observables to these traces. ST3_pairC, ST4_pairC and pairC_wordTraces refute the previous channel-family uniqueness route in their exact scope, not every conceivable observational carrier.

Required revisions before landing.

1. Preserve rather than over-delete independent time reversal, phase and other structural observations that do not depend on the refuted old lemma; qualify each by the actual allowed relabelling group.
2. Separate fixed-interface coherent-channel equivalence, population-only equivalence and all-partitions equivalence. With restricted hidden-only (i) and exact decoupled (iii), Pair C plus the balanced-word-trace invariant refutes exhaustiveness for fixed-interface channel equivalence, subject to direct verification of the chain invariant. Population-level fibre-dependent relabellings leave probabilities invariant, and Pair C is absorbed under that broader relation. All-partitions completeness remains open. The unqualified 'neither proved nor refuted' is too weak for the first relation.
3. Correct Theorem 24's soundness and definition dependencies in the integrated preview Foundational reconciliation: integrate #992 and preserve recovered theorem scope #982; do not pretend SC-44 lands coherently alone. Retain the frozen WTS research family at kernel-only; Proposition 24.2 uses its separate canonical coverage entry.
4. Reconcile downstream Substratum, chapter and Introduction claims; rerun architecture and coverage checks, regenerate canonical TeX/PDF. No broad checker exemption merely to silence failures.
5. Exact-head independent re-review of the integrated correction, and verification of the direct Lean statements, before any merge.

Status: REVISE / OPEN. This comment does not change branch content, accept a proof beyond the stated hypotheses, authorize a workflow dispatch, or approve merging. The intended integration vehicle is draft #982; this PR stays an independent audit record.