arisesFromSubstrateAccess_of_pureTensorFactorization
plain-language theorem explainer
Pure-tensor factorization of a joint operator forces the channel response to arise from substrate access whenever the matter factor is nonzero at some coordinate. Gravity-track workers cite this to bridge the older factorization hypothesis to the Session 113 substrate-locality principle. The proof builds access data from the factorization witness and cancels the calibration scalar by direct rewriting on the induced-channel formula.
Claim. Let $R_J$ be a $\mathbb{C}$-linear operator on the joint substrate $\mathrm{Signal}_8\otimes\mathrm{Signal}_8$, and let $R_M,R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$. If $R_J$ admits a pure-tensor factorization through $R_M$ and $R_C$, and if there exist a reference state $\psi_0$ and a coordinate $i_0\in\{0,\ldots,7\}$ with $(R_M\psi_0)(i_0)\neq 0$, then $R_C$ arises from substrate access of $R_J$: there exist access data making $R_C$ equal the induced channel harvested from $R_J$.
background
This module (Gravity Track 2.C) closes the gap left after Session 111's section-readout retirement. Session 111 showed that a nonzero matter-section readout of a linear joint operator is forced amplitude-linear; pure-tensor factorization was a sufficient but non-necessary route to that readout law. The remaining operational assumption was that the physical channel is obtained by such a readout. Substrate locality replaces that assumption: every operational channel on the joint substrate is harvested by fixing a matter reference $\psi_0$, applying the joint operator $R_J$ once, reading a channel coordinate $i_0$, and normalising by a calibration scalar $\chi\neq 0$.
Concretely, $R_C$ arises from substrate access of $R_J$ when there exist access data such that $R_C$ equals the induced channel $R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. Under that principle, section readout is the definition of how the operational channel is read off $R_J$, not an extra hypothesis. The eight-tick register $\mathrm{Signal}_8$ is the discrete recognition carrier (T7 octave period $2^3$).
The pure-tensor factorization hypothesis is the older structural assumption that $R_J$ splits as a product of a matter map and a channel map. This theorem shows that factorization, plus a single nonzero matter coordinate, already supplies substrate-access data.
proof idea
Term-mode construction of the existential. Package the given reference state $\psi_0$, coordinate $i_0$, and scalar $\chi:=(R_M\psi_0)(i_0)$ (nonzero by hypothesis) into substrate-access data. It remains to check that the induced channel for those data equals $R_C$. After funext on the channel argument $\varphi$ and unfolding the induced-channel definition, the goal is the scalar identity
$R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$.
Rewrite with the insert-first evaluation rule, the pure-tensor factorization hypothesis, the extract-second-on-tensor rule, and scalar cancellation (smul_smul, inv_mul_cancel₀, one_smul). The calibration inverse cancels against $\chi$, leaving $R_C\varphi$ on the nose.
why it matters
This is the bridge lemma from the older pure-tensor factorization language to the Session 113 substrate-access principle. Downstream, canonicalCyclicJointOperator_arisesFromRecognitionProbe applies it to the canonical recognition-coupled joint operator with the constant-1 matter reference and coordinate 0, making the substrate-access proposition non-vacuously inhabited for the recognition probe. That inhabitant feeds the certificate substrateLocalAccessCert, which packages the full implication chain: substrate access implies joint section readout, which implies amplitude-linearity of the channel, and collapses density-only channels.
In the module's stated chain, substrate access is the substantive principle; section readout and amplitude-linearity are consequences. The result therefore retires factorization as a free-standing channel hypothesis wherever a nontrivial matter coordinate is available. Framework landmarks in play are the eight-tick octave (T7) as the carrier of $\mathrm{Signal}_8$ and the recognition-probe coupling that realises the canonical joint operator. No open sorry remains in this module; the theorem is part of the 2026-05-22 structural closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.