substrateSemanticsUnconditionalCert
plain-language theorem explainer
Packages five unconditional Track 2.C results into one master certificate: every amplitude-linear channel on the eight-tick signal arises from substrate access; substrate access characterises amplitude-linearity; density-only amplitude-linear channels vanish; no nontrivial such channel exists; and the universal witness operator induces its linear map under canonical access. Gravity-track auditors cite it as the closed status object for substrate-access forcing. Construction is a structure instance wiring the five named theorems.
Claim. There is a certificate assembling five facts on channel responses $R_C:\mathrm{Signal}_8\to\mathrm{Signal}_8$: (i) every amplitude-linear $R_C$ arises from substrate access of some $\mathbb{C}$-linear joint operator on the joint substrate; (ii) $R_C$ is amplitude-linear if and only if it arises from such access; (iii) any amplitude-linear density-only $R_C$ satisfies $R_C\varphi=0$ for all $\varphi$; (iv) no nontrivial amplitude-linear density-only $R_C$ exists; (v) the universal substrate-access operator built from a witness $L$ induces exactly $L$ under canonical probe access.
background
Track 2.C studies operational recognition observables on the joint substrate: channel responses $R_C$ on the eight-tick signal space $\mathrm{Signal}_8$. Amplitude-linearity means $R_C$ is induced by some $\mathbb{C}$-linear map $L:\mathrm{Signal}_8\to\mathrm{Signal}_8$. Substrate access means $R_C$ is recovered by preparing a matter probe, applying a joint linear operator once, and reading a calibrated channel coordinate (the principle formerly encoded as a load-bearing hypothesis).
Earlier sessions reduced forcing hypotheses step by step (factor-product, then per-section readout, then substrate locality). This module retires the substrate-locality principle itself: every amplitude-linear $R_C$ arises from the universal joint operator $\mathrm{id}\otimes L$ under canonical access $(\psi_0=1,i_0=0,\chi=1)$. The master certificate structure records universality, the iff characterisation, the unconditional density-only collapse, the no-go, and the witness calculation that makes access universal.
proof idea
One structure instance of the master certificate type. Each field is filled by a prior theorem in the same module: universality by the construction that builds the universal joint operator from the amplitude-linear witness and canonical access; characterisation by the iff between amplitude-linearity and existence of a substrate-access witness; density-only collapse by reducing to the already-proved zero identity for amplitude-linear density-only channels; the no-go by the corresponding nonexistence statement; and the witness calculation by the identity that the universal operator induces exactly the witness linear map under canonical access. No new reasoning beyond packaging.
why it matters
This is the status object for Gravity Track 2.C unconditional closure: substrate access is derived from amplitude-linearity rather than assumed, so the density-only no-go no longer needs a separate access hypothesis. Downstream, the inhabitedness theorem simply wraps this value to exhibit a nonempty certificate type, and the module's one-statement unconditional theorem sits in the same closing section.
In framework terms it finishes the substrate-semantics half of the quantum-channel gravity track: operational observables on the eight-tick octave (T7) that are amplitude-linear are exactly those realised by joint linear access on the recognition substrate. The former substrate-access principle is no longer load-bearing; it is equivalent to the semantic minimum any operational channel must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.