substrateLocalAccessCert_inhabited
plain-language theorem explainer
The substrate-locality master certificate is non-vacuously inhabited: a complete package records that measurement-access on the joint substrate forces section readout, amplitude-linearity, and the density-only no-go. Gravity and quantum-channel workers cite it to discharge the Session 113 cert in one step. The proof is a one-line inhabitant witness of the pre-built certificate value.
Claim. The type of substrate-locality certificates is nonempty: there exists a package asserting that whenever a joint operator $R_J$ and channel $R_C$ arise from substrate access on $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$, the channel is a joint section readout and is amplitude-linear; any density-only response collapses to zero; and a canonical recognition-probe inhabitant witnesses non-vacuity.
background
Gravity Track 2.C closes the gap left by Session 111. Session 111 showed that a nonzero matter-section readout of a linear joint operator forces the channel to be amplitude-linear. What remained was the operational claim that the physical channel is obtained by such a readout.
Substrate locality (measurement-access) supplies that claim at the substrate level: every operational channel on the joint space $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ is harvested by fixing a matter reference $\psi_0$, applying a joint operator $R_J$ once, extracting a channel coordinate $i_0$, and normalising by a calibration scalar $\chi \neq 0$. The induced formula defines $R_C$ and is automatically a joint section readout.
The master certificate structure packages the full implication chain: substrate access implies section readout, which implies amplitude-linearity; a density-only no-go; and a non-vacuous canonical recognition-coupling inhabitant. This theorem asserts that package is inhabited.
proof idea
One-line term proof. The certificate value substrateLocalAccessCert is already assembled in-module from the sibling lemmas (access implies section readout; access forces amplitude-linearity; density-only channels vanish under access; the recognition-probe construction inhabits access). The proof simply wraps that value as an inhabitant of Nonempty SubstrateLocalAccessCert.
why it matters
This is the Session 113 one-statement closure for substrate locality. Section readout is no longer an assumption: it is derived from the measurement-access principle plus joint linearity. The factor-product theorem (Sessions 85-88) and the amplitude-linear forcing of Session 111 become corollaries of the packaged chain.
In the Recognition framework this sits one level deeper in the substrate axiomatisation than Session 111. The eight-tick joint substrate $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$ is the operational arena tied to the T7 octave. No downstream dependents are recorded yet; the cert is the terminal structural seal of the module.
The remaining unconditional target, named in the module doc, is to derive the access proposition itself from T0-T8 alone: every operational recognition observable on the joint substrate must be of induced form. That is substrate semantics and the next session-scale step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.