diff --git a/papers/GR.md b/papers/GR.md
index cd8d16a72..3a18ba389 100644
--- a/papers/GR.md
+++ b/papers/GR.md
@@ -257,7 +257,7 @@ $$\boxed{\begin{aligned}&\text{implementation locality} + \text{phase-free richn
 
 holds on every nonempty finite carrier. It refines the OI⁺ characterization, and it is not a claim that bare observation incompleteness entails these principles: the normalization half of operational validity is a consequence of implementation generation, an intervention realized by one protocol preserving probability in aggregate, and neither principle is supplied by the others, the witnesses being stated for the Lie-rank condition that phase-free richness supplies (kernel: `redundancy_fails`, `lieRank_not_redundant`). The nonclassical repertoire the equivalence consumes is one continuously driven transition together with the exchanges of distinguishable states; the quarter phase is dispensable at every level. The exchange clause is not reducible to the powers of a single cyclic permutation: on an even carrier one driven transition with one full cycle generates a conjugate of the real antisymmetric matrices, which reaches no population difference (kernel: `not_hControl_evenCycle`), so one full cycle together with one adjacent exchange is the two-element discrete form the kernel formalizes, sufficient for every exchange (kernel: `phaseFree_of_cyclic`), with no claim that a smaller discrete resource is excluded, and no stronger minimality of the one driven transition is claimed. Whether that driven transition can be supplied by a discrete resource is the question of the substratum-source form below. Inverse accessibility is not a hypothesis of the equivalence: Lie-rank richness gives full composite unitary control unconditionally, and on a well-formed theory full control yields inverse accessibility, well-formedness being supplied by implementation locality with embedded observation (kernel: `inverseAccessibility_of_lieRank`). An implementation class closed under the adjoint remains a property of exact quantum mechanics (kernel: `reversibleImplementationLocality_of_qm` in `OIBridge/MicroscopicReversibility.lean`), and, with the other two principles, the class with that closure and the class without it characterize the same theory (kernel: `oiPlusPos_iff_oiPlusElem`).
 
-**Substratum-source form.** The three primitive-source principles are jointly supplied by one object: an implementation architecture — a class of admissible implementation operators closed under the operations of a finite operational theory — that is stable under an uncoupled spectator, invariant under relabelling of the carrier, closed under the adjoint, and drives the elementary transitions. A theory generated by such an architecture is exact finite endomorphic operational quantum mechanics on every nonempty finite carrier, and that quantum mechanics is generated by one (kernel: `genTheory_qm_of_quantumArchitecture`, `qm_generated_by_quantumArchitecture` in `OIBridge/SubstratumSource.lean`). The concrete OI substratum — finite states and bijective microscopic dynamics (Axiom 2) — together with one further intervention principle, that a relative phase on a single state is a selectable intervention at every level, supplies the structural part in full. The phase intervention enters as an assumption on the substratum class, not as a consequence of the finite states with the bijective read-write dynamics: every isometry that dynamics and the stated observer access supply carries the all-ones vector to a multiple of itself; on every finite carrier with two or more states, the theory generated by an architecture whose admissible isometries do so fails the requirement of a quarter phase on every state at every level, the failure being exhibited at level one, with no claim that the quarter phase is unavailable at each composite level; and the quarter phase carries that vector off its ray (kernel: `permClass_onesFixing`, `onesFixing_not_phasesAvailable`, `substratumClass_not_onesFixing` in `OIBridge/PhaseSource.lean`). An operator carrying the all-ones vector off its ray is therefore necessary to any access that supplies the phases, and is not shown sufficient; the access assumed is the quarter-phase intervention itself, a member of the class as stated (kernel: `phase_monomial` in `OIBridge/SubstratumInterface.lean`). The interventions of the substratum so stated have monomial observable operators, a permutation of a diagonal (kernel: `bijectiveOperator_monomial`, `phaseOperator_monomial` in `OIBridge/SubstratumInterface.lean`), and that class, with nothing added, is closed under composition, coarse-graining, and ancilla blocks, stable under an uncoupled spectator, invariant under relabelling, and closed under the adjoint — the reversal of a bijective intervention is the inverse bijection and the reversal of a phase is its conjugate — with the exchanges of distinguishable states and the phases among its members (kernel: `substratumClass_structurallyClosed`, `bijectiveOperator_conjTranspose`, `phaseOperator_conjTranspose` in `OIBridge/StructuralClosure.lean`). What it does not supply, under finite bijective read-write dynamics, is the continuously tunable state-mixing operation: a monomial conjugation preserves diagonal states, whereas a continuously driven transition between two distinguishable states passes through operators with two nonzero entries in one row, which no bijection realizes. Finite reversible read-write dynamics, even with genuine hidden-memory and readback behavior, does not itself generate quantum state mixing: a selectable local coupling that is a bijection at every parameter value induces only permutation operators, a strict interpolation toward the exchange is not a bijection, and the memory-swap coupling moves information bidirectionally while remaining monomial (kernel: `readWriteSourced_not_qm`, `offDiagonal_interp_not_monomial`, `readWriteControl_independent` in `OIBridge/ReadWriteControl.lean`; `substratum_residual` in `OIBridge/StructuralClosure.lean`). Adding that one operation as an empirical controllability resource completes the quantum architecture: a structurally closed extension of the substratum class is a quantum architecture exactly when it drives the elementary transitions, it generates exact finite endomorphic operational quantum mechanics on every nonempty finite carrier when it does, and quantum mechanics is generated by such an extension (kernel: `substratum_extension_quantum_iff_drives`, `substratum_plus_control_qm`, `qm_generated_by_substratum_extension`):
+**Substratum-source form.** The three primitive-source principles are jointly supplied by one object: an implementation architecture — a class of admissible implementation operators closed under the operations of a finite operational theory — that is stable under an uncoupled spectator, invariant under relabelling of the carrier, closed under the adjoint, and drives the elementary transitions. A theory generated by such an architecture is exact finite endomorphic operational quantum mechanics on every nonempty finite carrier, and that quantum mechanics is generated by one (kernel: `genTheory_qm_of_quantumArchitecture`, `qm_generated_by_quantumArchitecture` in `OIBridge/SubstratumSource.lean`). The concrete OI substratum — finite states and bijective microscopic dynamics (Axiom 2) — together with one further intervention principle, that a relative phase on a single state is a selectable intervention at every level, supplies the structural part in full. The phase intervention enters as an assumption on the substratum class, not as a consequence of the finite states with the bijective read-write dynamics: every isometry that dynamics and the stated observer access supply carries the all-ones vector to a multiple of itself; on every finite carrier with two or more states, the theory generated by an architecture whose admissible isometries do so fails the requirement of a quarter phase on every state at every level, the failure being exhibited at level one, with no claim that the quarter phase is unavailable at each composite level; and the quarter phase carries that vector off its ray (kernel: `permClass_onesFixing`, `onesFixing_not_phasesAvailable`, `substratumClass_not_onesFixing` in `OIBridge/PhaseSource.lean`). An operator carrying the all-ones vector off its ray is therefore necessary to any access that supplies the phases, and is not shown sufficient; the access assumed is the quarter-phase intervention itself, a member of the class as stated (kernel: `phase_monomial` in `OIBridge/SubstratumInterface.lean`). The interventions of the substratum so stated have monomial observable operators, a permutation of a diagonal (kernel: `bijectiveOperator_monomial`, `phaseOperator_monomial` in `OIBridge/SubstratumInterface.lean`), and that class, with nothing added, is closed under composition, coarse-graining, and ancilla blocks, stable under an uncoupled spectator, invariant under relabelling, and closed under the adjoint — the reversal of a bijective intervention is the inverse bijection and the reversal of a phase is its conjugate — with the exchanges of distinguishable states and the phases among its members (kernel: `substratumClass_structurallyClosed`, `bijectiveOperator_conjTranspose`, `phaseOperator_conjTranspose` in `OIBridge/StructuralClosure.lean`). What it does not supply, under finite bijective read-write dynamics, is the continuously tunable state-mixing operation: a monomial conjugation preserves diagonal states, whereas a continuously driven transition between two distinguishable states passes through operators with two nonzero entries in one row, which no bijection realizes. Finite reversible read-write dynamics, even with a nontrivial reversible read-write coupling, does not itself generate quantum state mixing: a selectable local coupling that is a bijection at every parameter value induces only permutation operators, a strict interpolation toward the exchange is not a bijection, and the memory-swap coupling moves information bidirectionally while remaining monomial (kernel: `readWriteOperator_eq_perm`, `offDiagonal_interp_not_monomial`, `readWriteControl_independent` in `OIBridge/ReadWriteControl.lean`; `substratum_residual` in `OIBridge/StructuralClosure.lean`). Adding that one operation as an empirical controllability resource completes the quantum architecture: a structurally closed extension of the substratum class is a quantum architecture exactly when it drives the elementary transitions, it generates exact finite endomorphic operational quantum mechanics on every nonempty finite carrier when it does, and quantum mechanics is generated by such an extension (kernel: `substratum_extension_quantum_iff_drives`, `substratum_plus_control_qm`, `qm_generated_by_substratum_extension`):
 
 $$\boxed{\begin{aligned}&\text{current OI substratum} + \text{continuous off-diagonal controllability}\\ &\qquad \iff\; \text{exact finite endomorphic operational QM}\end{aligned}}$$
 
diff --git a/papers/GR.pdf b/papers/GR.pdf
index 83ad00f97..b3268feb9 100644
Binary files a/papers/GR.pdf and b/papers/GR.pdf differ
diff --git a/papers/GR.tex b/papers/GR.tex
index cfe6a0106..c424b4140 100644
--- a/papers/GR.tex
+++ b/papers/GR.tex
@@ -1847,13 +1847,13 @@ \subsubsection{3.3 Gauge-fixing and the dimensional
 states, whereas a continuously driven transition between two
 distinguishable states passes through operators with two nonzero entries
 in one row, which no bijection realizes. Finite reversible read-write
-dynamics, even with genuine hidden-memory and readback behavior, does
+dynamics, even with a nontrivial reversible read-write coupling, does
 not itself generate quantum state mixing: a selectable local coupling
 that is a bijection at every parameter value induces only permutation
 operators, a strict interpolation toward the exchange is not a
 bijection, and the memory-swap coupling moves information
 bidirectionally while remaining monomial (kernel:
-\texttt{readWriteSourced\_not\_qm},
+\texttt{readWriteOperator\_eq\_perm},
 \texttt{offDiagonal\_interp\_not\_monomial},
 \texttt{readWriteControl\_independent} in
 \texttt{OIBridge/ReadWriteControl.lean}; \texttt{substratum\_residual}
@@ -5506,4 +5506,4 @@ \subsection{References}\label{references}}
 arXiv:quant-ph/0407049.
 
 \end{document}
-% source-sha256: a475a2a8af62ea262c9981a9e173253105a1234b18259f597f604d5201784992
+% source-sha256: 23aef3ee734278e9ed3cacb401a200027158925ef7dcc06a8b266c4dfd7c87a2
diff --git a/papers/Main.md b/papers/Main.md
index 4a7ed0a8e..528d1e916 100644
--- a/papers/Main.md
+++ b/papers/Main.md
@@ -585,7 +585,7 @@ The operational-completion theorem also admits a physically layered formulation.
 
 $$\mathrm{OI}^{+}\;\iff\;\text{exact finite endomorphic operational QM}.$$
 
-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`). This is a characterization of a quantum-complete extension of OI, not a claim that bare OI entails the added principles; the OI-core clause becomes logically redundant once the reversible-control condition is present. On a general carrier OI⁺ consists of well-formedness and the three added principles, with no OI-core clause; the OI-core clause is defined on the qubit, where it does not change the class (kernel: `carrier_general_oiPlus`, with directions `qm_of_oiPlus` and `oiPlus_of_qm`, and `oiPlus_qubit_iff` in `OIBridge/CarrierGeneralOIPlus.lean`). A primitive-source refinement restates the three added principles at the level of physical implementations and embedded observers — implementation locality, phase-free richness — one continuously driven transition and the exchanges of distinguishable states, with no phase operation — and embedded observation, with no closure of the implementations under the adjoint and no inverse accessibility assumed — equivalent to the same operational quantum mechanics on every nonempty finite carrier, inverse accessibility following on any well-formed theory (kernel: `carrier_general_oiPlusMin`, `oiPlusMin_iff_qm` in `OIBridge/MinimalRepertoire.lean`; `carrier_general_oiPlusPos` in `OIBridge/PositivePackage.lean`, `inverseAccessibility_of_lieRank` in `OIBridge/MicroscopicReversibility.lean`). A substratum-source form completes that refinement: the concrete OI substratum supplies the structural architecture — closure under composition and coarse-graining, stability under an uncoupled spectator, relabelling invariance, reversibility, the exchanges of distinguishable states, and, as a stated intervention principle rather than a consequence of its finite states and bijective dynamics, the phases — but, under finite bijective read-write dynamics, not the continuously tunable state-mixing operation; with that one operation added as an empirical controllability resource it is equivalent to the same operational quantum mechanics on every nonempty finite carrier, while finite reversible read-write dynamics, even with genuine hidden-memory and readback behavior, does not itself generate quantum state mixing (kernel: `substratum_plus_control_qm`, with the converse `qm_generated_by_substratum_extension`, in `OIBridge/StructuralClosure.lean`, `readWriteSourced_not_qm` in `OIBridge/ReadWriteControl.lean`). Its typed form removes the endomorphic qualifier: under the carrier-general typed operational interface — identity, composition, coarse-graining, relabelling, uniform finite attachment, discard, and factor readout, an interface that itself carries no quantum content — the same equivalence holds with exact finite-dimensional typed operational quantum mechanics, operations between any two nonempty finite carriers included, so the remaining qualifier is finite-dimensional rather than endomorphic (kernel: `typed_determined_iff` in `OIBridge/TypedCompletion.lean`, `typed_determined_of_oiPlusMin` in `OIBridge/TypedPositive.lean`). The finite theory admits a canonical infinite-region completion without a continuum limit: the finite regions of the fixed-spacing lattice carry full matrix algebras joined by compatible injective unital embeddings with observables of disjoint regions commuting, the norm completion of their union is a quasilocal $C^{*}$-algebra on which every consistent family of finite-region density matrices is a state and the reversible finite-range substratum update is an isometric $*$-automorphism, and any system carrying the same local stages is canonically and uniquely $*$-isomorphic to it, intertwining the dynamics; this removes the finite-region cutoff for the algebra, the state space, and the OI-induced discrete dynamics rather than characterizing all infinite-dimensional quantum instruments or all locality-preserving quantum dynamics; the lattice spacing stays fundamental, no Hilbert-space representation and no superselection sector is selected at the level of the laws, the restriction to the substratum-induced dynamics is a theorem rather than a convention — a phase automorphism at one site preserves locality without arising from any reversible finite-range bijection — and, while the update is joined to the identity by an exact strongly continuous path of $*$-automorphisms of that algebra, with no one-parameter-group law established and no generator exhibited, a continuous-time Hamiltonian law remains additional structure (kernel: `closure_iUnion_stage`, `quasiState_unique` in `OIBridge/QuasilocalAlgebra.lean`, `canonEquiv`, `phaseQ_ne_heisQ` in `OIBridge/QuasilocalCharacterization.lean`; `driveQ_isContinuousPath`, `driveQ_smul`, `driveQ_one_eq_heisQ` in `OIBridge/SecondOrderDrive.lean`). Within the structural architecture the substratum supplies, with the phase intervention stated, exact finite endomorphic operational quantum mechanics holds exactly when one continuous layer flow of an involution of the configuration space moving some configuration is an available operation at every level and every intermediate time, the executability of that flow being an assumption not derived by configuration-level generation, as the phase intervention is an assumption on the substratum class and not a consequence of the finite states with the bijective dynamics (kernel: `derivedOI_qm_iff_layerFlowExecutable'` in `OIBridge/DerivedQ3.lean`, `substratumTheory_not_layerFlowExecutable` in `OIBridge/LiftAudit.lean`). The stated substratum dynamics with the observer's read and write access do not source that executability, the layers being available at time one and not at intermediate times, and the observer-level lift, in every formulation stated that lands in the operational interface, derives neither a non-monomial admissible operator nor the layer flow, the site-space wave-operator formulation being unresolved rather than excluded (kernel: `obs_not_layerFlowExecutable` in `OIBridge/ExecSource.lean`, `coherentLiftClass_eq_substratumClass` in `OIBridge/LiftSource.lean`).
+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`). This is a characterization of a quantum-complete extension of OI, not a claim that bare OI entails the added principles; the OI-core clause becomes logically redundant once the reversible-control condition is present. On a general carrier OI⁺ consists of well-formedness and the three added principles, with no OI-core clause; the OI-core clause is defined on the qubit, where it does not change the class (kernel: `carrier_general_oiPlus`, with directions `qm_of_oiPlus` and `oiPlus_of_qm`, and `oiPlus_qubit_iff` in `OIBridge/CarrierGeneralOIPlus.lean`). A primitive-source refinement restates the three added principles at the level of physical implementations and embedded observers — implementation locality, phase-free richness — one continuously driven transition and the exchanges of distinguishable states, with no phase operation — and embedded observation, with no closure of the implementations under the adjoint and no inverse accessibility assumed — equivalent to the same operational quantum mechanics on every nonempty finite carrier, inverse accessibility following on any well-formed theory (kernel: `carrier_general_oiPlusMin`, `oiPlusMin_iff_qm` in `OIBridge/MinimalRepertoire.lean`; `carrier_general_oiPlusPos` in `OIBridge/PositivePackage.lean`, `inverseAccessibility_of_lieRank` in `OIBridge/MicroscopicReversibility.lean`). A substratum-source form completes that refinement: the concrete OI substratum supplies the structural architecture — closure under composition and coarse-graining, stability under an uncoupled spectator, relabelling invariance, reversibility, the exchanges of distinguishable states, and, as a stated intervention principle rather than a consequence of its finite states and bijective dynamics, the phases — but, under finite bijective read-write dynamics, not the continuously tunable state-mixing operation; with that one operation added as an empirical controllability resource it is equivalent to the same operational quantum mechanics on every nonempty finite carrier, while finite reversible read-write dynamics, even with a nontrivial reversible read-write coupling, does not itself generate quantum state mixing (kernel: `substratum_plus_control_qm`, with the converse `qm_generated_by_substratum_extension`, and `readWriteOperator_supplied` and, on the two-state carrier, `substratumGen_not_control`, in `OIBridge/StructuralClosure.lean`, `readWriteControl_independent` in `OIBridge/ReadWriteControl.lean`). Its typed form removes the endomorphic qualifier: under the carrier-general typed operational interface — identity, composition, coarse-graining, relabelling, uniform finite attachment, discard, and factor readout, an interface that itself carries no quantum content — the same equivalence holds with exact finite-dimensional typed operational quantum mechanics, operations between any two nonempty finite carriers included, so the remaining qualifier is finite-dimensional rather than endomorphic (kernel: `typed_determined_iff` in `OIBridge/TypedCompletion.lean`, `typed_determined_of_oiPlusMin` in `OIBridge/TypedPositive.lean`). The finite theory admits a canonical infinite-region completion without a continuum limit: the finite regions of the fixed-spacing lattice carry full matrix algebras joined by compatible injective unital embeddings with observables of disjoint regions commuting, the norm completion of their union is a quasilocal $C^{*}$-algebra on which every consistent family of finite-region density matrices is a state and the reversible finite-range substratum update is an isometric $*$-automorphism, and any system carrying the same local stages is canonically and uniquely $*$-isomorphic to it, intertwining the dynamics; this removes the finite-region cutoff for the algebra, the state space, and the OI-induced discrete dynamics rather than characterizing all infinite-dimensional quantum instruments or all locality-preserving quantum dynamics; the lattice spacing stays fundamental, no Hilbert-space representation and no superselection sector is selected at the level of the laws, the restriction to the substratum-induced dynamics is a theorem rather than a convention — a phase automorphism at one site preserves locality without arising from any reversible finite-range bijection — and, while the update is joined to the identity by an exact strongly continuous path of $*$-automorphisms of that algebra, with no one-parameter-group law established and no generator exhibited, a continuous-time Hamiltonian law remains additional structure (kernel: `closure_iUnion_stage`, `quasiState_unique` in `OIBridge/QuasilocalAlgebra.lean`, `canonEquiv`, `phaseQ_ne_heisQ` in `OIBridge/QuasilocalCharacterization.lean`; `driveQ_isContinuousPath`, `driveQ_smul`, `driveQ_one_eq_heisQ` in `OIBridge/SecondOrderDrive.lean`). Within the structural architecture the substratum supplies, with the phase intervention stated, exact finite endomorphic operational quantum mechanics holds exactly when one continuous layer flow of an involution of the configuration space moving some configuration is an available operation at every level and every intermediate time, the executability of that flow being an assumption not derived by configuration-level generation, as the phase intervention is an assumption on the substratum class and not a consequence of the finite states with the bijective dynamics (kernel: `derivedOI_qm_iff_layerFlowExecutable'` in `OIBridge/DerivedQ3.lean`, `substratumTheory_not_layerFlowExecutable` in `OIBridge/LiftAudit.lean`). The stated substratum dynamics with the observer's read and write access do not source that executability, the layers being available at time one and not at intermediate times, and the observer-level lift, in every formulation stated that lands in the operational interface, derives neither a non-monomial admissible operator nor the layer flow, the site-space wave-operator formulation being unresolved rather than excluded (kernel: `obs_not_layerFlowExecutable` in `OIBridge/ExecSource.lean`, `coherentLiftClass_eq_substratumClass` in `OIBridge/LiftSource.lean`).
 
 **Passive observation, kept apart from the characterization.** Four statements about passive observation stand beside the equivalence above and enter none of its hypotheses or conclusions. Complete passive observation of a finite-dimensional observable algebra in block-diagonal form — observation by a passive instrument, one whose branches leave the block projectors fixed — is possible exactly when the algebra is commutative: some passive instrument separates its states exactly when the algebra is commutative, and every passive instrument induces a classical stochastic observation of the algebra's center (kernel: `complete_passive_iff_commutative`, `central_classification` in `OIBridge/CentralObservation.lean`; `no_complete_passive_observation` in `OIBridge/PassiveObservation.lean`). Quantum noncommutativity cannot coexist with complete passive observation. This is theory-insensitive: passive incompleteness holds in every finite operational theory on a carrier with two or more states, so it carries no information about whether the OI core is realized; the implication from the core to passive incompleteness holds vacuously, and its converse fails, witnessed by a theory that is passively incomplete and lacks the core (kernel: `passivelyIncomplete_of_card`, `oiCore_to_passive_vacuous`, `passivelyIncomplete_without_oiCore`, `passive_nondiscriminating` in `OIBridge/PassiveIndependence.lean`). Passive incompleteness is therefore not evidence for a hidden ontology, and nothing here says that quantum mechanics rests on observation incompleteness: the containment in the other direction, that exact finite quantum mechanics realizes the sealed core, is a consequence of full control and nothing more (kernel: `qm_implies_oiCore` in `OIBridge/CompletedOI.lean`, through `realizesSealedOICore_of_control` in `OIBridge/OIRealization.lean`). A passive internal observer, whose outcome is a function of a register read on block-diagonal states, can only read an existing record: each of its branches is the record projection $\rho \mapsto P_o \rho P_o$, with outcome law $\mathrm{tr}(P_o \rho P_o)$ (kernel: `internal_branch_eq_blockPart`, `internal_outcome_law` in `OIBridge/InternalObserver.lean`), and creating a genuinely new record changes the joint system, the recorder that writes the register being not passive on the record-block algebra (kernel: `recordInstr_writes`, `recordInstr_not_passive`, `no_full_passive_self_record`). All four statements are finite-dimensional, and none bears on the equivalence.
 
diff --git a/papers/Main.pdf b/papers/Main.pdf
index 4049c8062..262e86684 100644
Binary files a/papers/Main.pdf and b/papers/Main.pdf differ
diff --git a/papers/Main.tex b/papers/Main.tex
index 6eae3982e..424a817a2 100644
--- a/papers/Main.tex
+++ b/papers/Main.tex
@@ -3916,12 +3916,14 @@ \subsubsection{3.4 The Characterization Theorem: Necessity of the
 operation; with that one operation added as an empirical controllability
 resource it is equivalent to the same operational quantum mechanics on
 every nonempty finite carrier, while finite reversible read-write
-dynamics, even with genuine hidden-memory and readback behavior, does
+dynamics, even with a nontrivial reversible read-write coupling, does
 not itself generate quantum state mixing (kernel:
 \texttt{substratum\_plus\_control\_qm}, with the converse
-\texttt{qm\_generated\_by\_substratum\_extension}, in
+\texttt{qm\_generated\_by\_substratum\_extension}, and
+\texttt{readWriteOperator\_supplied} and, on the two-state carrier,
+\texttt{substratumGen\_not\_control}, in
 \texttt{OIBridge/StructuralClosure.lean},
-\texttt{readWriteSourced\_not\_qm} in
+\texttt{readWriteControl\_independent} in
 \texttt{OIBridge/ReadWriteControl.lean}). Its typed form removes the
 endomorphic qualifier: under the carrier-general typed operational
 interface --- identity, composition, coarse-graining, relabelling,
@@ -5968,4 +5970,4 @@ \subsection{REFERENCES}\label{references}}
 stochastic-quantum correspondence,'' arXiv:2602.23491v1 (2026).
 
 \end{document}
-% source-sha256: ca76995be20fe9c3777344b6d009b0eb93d9828f5c9d848388725bab66b882ac
+% source-sha256: bf425ea68a20749de1a496a1f18c654452c86e8c9ff6b9f541fb488b8066e333
diff --git a/verification/README.md b/verification/README.md
index b40229a75..9a14274b7 100644
--- a/verification/README.md
+++ b/verification/README.md
@@ -294,8 +294,8 @@ genuine two-state rotation is not monomial (`SubstratumInterface.monomialSource_
 `rot_not_monomial`) — finite bijective dynamics alone does not supply the decisive operator. Its third entry audits the
 decisive escape route, read-write coupling, and returns the no-go for the current axioms: a
 read-write family (a selectable local coupling, bijective at every parameter value) induces only
-permutation operators, so a read-write-sourced theory is a monomial source and is not QM
-(`ReadWriteControl.readWriteSourced_not_qm`); a strict interpolation toward the swap is not a
+permutation operators, which are monomial
+(`ReadWriteControl.readWriteOperator_monomial`); a strict interpolation toward the swap is not a
 bijection (`offDiagonal_interp_not_monomial`), so the tunable coupling produces no off-diagonal
 generator, and the memory-swap countercontrol shows bidirectional read-write is not off-diagonal
 controllability (`readWriteControl_independent`). Under the current axioms a continuously tunable