SubstrateAccessData
plain-language theorem explainer
Packages the three parameters of one recognition-probe measurement on the joint eight-tick substrate: a fixed matter reference state, a channel-side coordinate index in Fin 8, and a nonzero complex calibration. Anyone deriving operational channel responses from joint linear operators under substrate locality cites this bundle. As a structure definition it carries no proof obligation; it is the data type that induces the channel readout recipe.
Claim. A substrate access datum is a triple $(\psi_0, i_0, \chi)$ where $\psi_0$ is a matter probe state in the eight-component signal space, $i_0 \in \{0,\ldots,7\}$ is a channel-side readout coordinate, and $\chi \in \mathbb{C}$ is a nonzero calibration scalar. This is the data of one recognition-update measurement probe on the joint substrate $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$.
background
Gravity Track 2.C closes the gap left after Session 111's section-readout retirement. Session 111 showed that any nonzero matter-section readout of a linear joint operator is forced amplitude-linear; pure-tensor factorization is sufficient but not necessary. The remaining assumption was that the physical channel is operationally obtained by such a readout.
This module replaces that assumption by a substrate-level principle: every operational channel observable on the joint substrate is a recognition probe. Fix a matter reference state $\psi_0$, apply the joint linear operator $R_J$ once to the inserted pair, read the channel coordinate $i_0$, and normalise by a calibration $\chi \neq 0$. The eight-tick factor $\mathrm{Signal}_8$ is the discrete octave carrier (period $2^3$) of the recognition calculus.
The structure simply packages those three parameters. Downstream, the induced channel is defined by $R_C\varphi = \chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$, which is automatically a joint section readout.
proof idea
No proof: this is a structure definition (four fields, one of them a Prop inequality $\chi \neq 0$). It introduces the data type used by inducedChannel and by the predicate that a channel arises from substrate access. Field projections and the nonzero certificate are available by construction; no lemmas are applied.
why it matters
This is the data carrier for the Session 113 substrate locality / measurement-access principle. The implication chain in the module is: substrate access data for $(R_J,R_C)$ implies joint section readout, which implies the channel is amplitude-linear. Downstream, inducedChannel builds the operational readout from an access datum; ArisesFromSubstrateAccess is the existential wrapper; inducedChannel_isSectionReadout discharges the Session 111 hypothesis automatically; and physicalChannelLinearExtension supplies the explicit $\mathbb{C}$-linear witness $\chi^{-1}\cdot(\mathrm{extractSecond}_{i_0}\circ R_J\circ\mathrm{insertFirst},\psi_0)$ used in the physical-channel amplitude-linearity track. In RS terms it ties the eight-tick octave carrier to how gravity-side channel responses are harvested from joint substrate operators, without extra readout axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.