substrateSemanticsUnconditionalCert_inhabited
plain-language theorem explainer
The unconditional Track 2.C substrate-semantics certificate is inhabited: every amplitude-linear channel response on the eight-tick signal space arises from substrate access, the two notions characterise each other, and the density-only no-go needs no extra access hypothesis. Gravity and quantum-channel workers citing the Session 125 closure would point here. The proof is a one-line Nonempty witness packing the assembled certificate value.
Claim. The type of unconditional substrate-semantics certificates is nonempty. Such a certificate asserts: (i) every amplitude-linear channel response $R_C$ on the eight-tick signal space arises from substrate access via some $\mathbb{C}$-linear joint operator $R_J$ on the joint substrate; (ii) amplitude-linearity characterises substrate accessibility; (iii) the density-only no-go therefore holds with no further substrate-access hypothesis.
background
Track 2.C studies whether gravity-side channel responses on the eight-tick recognition register can be density-only. Earlier sessions reduced the load-bearing input from bare amplitude-linearity, to a factor-product hypothesis, to per-section readout, and finally (Session 124) to a named substrate locality / measurement-access principle: the channel is recovered by preparing a matter probe, applying one linear joint operator, and reading a calibrated channel coordinate.
This module retires that principle itself. Substrate access is shown to be forced by substrate semantics: for every amplitude-linear $R_C$ with witness $L$, the joint operator $\mathrm{id}\otimes L$ on the joint substrate induces $R_C$ under the canonical recognition probe $(\psi_0=1, i_0=0, \chi=1)$. Amplitude-linearity is thereby equivalent to arising from substrate access.
The master certificate structure packages three facts: universality of substrate access for amplitude-linear channels, the characterisation equivalence, and the unconditional density-only no-go. The present theorem only asserts that this certificate type is inhabited.
proof idea
One-line term proof. The certificate value substrateSemanticsUnconditionalCert has already been assembled in-module from the universality, characterisation, and unconditional no-go lemmas. The proof packs that value as the witness of Nonempty, i.e. ⟨substrateSemanticsUnconditionalCert⟩. No further tactic work.
why it matters
This is the inhabitance seal on the Session 125 unconditional closure of Gravity Track 2.C. The module status is theorem with zero sorry and zero RS-internal axiom: the substrate-access hypothesis is no longer an input on the chain; it is derived from amplitude-linearity via the universal-witness construction $\mathrm{id}\otimes L$.
Downstream, the sibling one-statement theorem restates the same closure in prose form. No further declarations currently depend on this inhabitance lemma (used-by count is zero); it exists so the certificate type can be treated as a proved fact rather than a hypothesis interface.
Framework context: the eight-tick register (T7) is the finite-dimensional signal space on which amplitude-linearity is stated. What remains open, as the module notes, is deriving amplitude-linearity itself for the physical channel response from the T0–T8 forcing chain. That is the next-session gap on this thread, not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.