SubstrateLocalAccessCert
plain-language theorem explainer
Certificate packing the substrate-locality implication chain for joint quantum channels on Signal8 ⊗ Signal8: access forces section readout, amplitude-linearity, and collapse of density-only responses, plus a pure-tensor factorization bridge and a canonical recognition-coupling witness. Gravity-track authors cite it when retiring classical mediators under measurement-access. It is a structure definition; the inhabitant wires already-proved sibling lemmas.
Claim. A substrate-locality certificate is a record of six facts: (1) if a channel $R_C$ arises from substrate access to a joint linear operator $R_J$, then a joint section-readout of $R_J$ by $R_C$ exists; (2) such access forces $R_C$ to be amplitude-linear; (3) access plus density-only forces $R_C\equiv 0$; (4) no nontrivial density-only channel arises from substrate access; (5) pure-tensor factorization of $R_J$ with a nonzero matter factor implies access for $R_C$; (6) the canonical cyclic joint operator with the recognition update arises from substrate access.
background
Gravity Track 2.C closes the measurement-access principle on the joint substrate $\mathrm{Signal8}\otimes\mathrm{Signal8}$. Session 111 already showed that a nonzero matter-section readout of a linear joint operator forces the channel to be amplitude-linear; pure-tensor factorization was sufficient but not necessary for that readout law. The remaining gap was operational: why should a physical channel be a section readout at all?
Substrate locality answers that. Operational access data fix a matter reference $\psi_0$, a coordinate $i_0$, and a calibration $\chi\neq 0$; the channel is then defined by $R_C\varphi=\chi^{-1}\cdot\mathrm{extractSecond}_{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$. By definition this is a joint section readout, so section readout ceases to be an extra hypothesis.
ArisesFromSubstrateAccess is the per-channel proposition: $R_C$ equals the induced channel for some access data. The certificate packages the full implication chain from that proposition through section readout and amplitude-linearity, together with the density-only no-go and a non-vacuous witness.
proof idea
No proof body: this is a structure whose fields are named propositions. The concrete inhabitant substrateLocalAccessCert fills each field by a one-line application of a sibling lemma: sectionReadout_of_arisesFromSubstrateAccess for the readout link; isAmplitudeLinear_channel_of_arisesFromSubstrateAccess for amplitude-linearity; the density-only collapse and existence-form no-go siblings for the classical-mediator ban; arisesFromSubstrateAccess_of_pureTensorFactorization for the factorization bridge; and canonicalCyclicJointOperator_arisesFromRecognitionProbe (via the recognition-probe access data) for the canonical witness. Inhabitation is then ⟨substrateLocalAccessCert⟩.
why it matters
This is the master cert for Track 2.C. Downstream, substrateLocalAccessCert is the unique noncomputable package of the six links, and substrateLocalAccessCert_inhabited records that the type is nonempty, enabling the one-statement substrate-locality theorem later in the module.
In the Recognition framework it retires the last operational assumption between joint linear dynamics and forced amplitude-linearity of the observed channel. Classical density-only mediators are ruled out once substrate access is granted, so gravity-side quantum channels cannot hide behind classical readout. The eight-tick register (Signal8, period $2^3$) is the carrier, tying the argument to the T7 octave structure. The canonical witness uses the recognition update as the physical coupling, so the cert is not a vacuous interface: at least one RS-native joint operator realises the whole chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.