SubstrateSemanticsUnconditionalCert
plain-language theorem explainer
Master certificate bundling the unconditional Track 2.C closure: every amplitude-linear eight-tick channel arises from joint-substrate access, amplitude-linearity is equivalent to that access form, and density-only channels collapse to zero with no extra hypothesis. Gravity and quantum-channel workers cite it as the single package of substrate-semantics universality. The declaration is a pure record type; the inhabited instance wires five already-proved component lemmas.
Claim. A certificate with five assertions: (i) every amplitude-linear map $R_C$ on the eight-tick signal space arises from some $\mathbb{C}$-linear operator on the joint substrate via substrate access; (ii) $R_C$ is amplitude-linear if and only if such an access witness exists; (iii) any amplitude-linear density-only channel vanishes on every signal; (iv) no nontrivial amplitude-linear density-only channel exists; (v) for every linear $L$ on the signal space, the universal substrate-access operator induced under canonical access recovers $L$ as the channel response.
background
Track 2.C studies operational recognition observables on the eight-tick register Signal8 and their lift to the joint substrate (matter probe tensor channel coordinate). An amplitude-linear channel is a response map that is $\mathbb{C}$-linear in the signal amplitudes. Substrate access means the response is recovered by preparing a fixed probe, applying one joint linear operator, and reading a calibrated coordinate; the module uses the canonical access triple (unit probe, coordinate index 0, unit calibration).
Earlier sessions reduced forcing of amplitude-linear channels first to a factor-product hypothesis, then to per-section readout, then to a named substrate-locality / measurement-access principle. This module's setting is the unconditional retirement of that principle: substrate access is no longer an input axiom but a derived characterisation of amplitude-linearity.
Density-only channels depend only on modulus-squared data. The no-go thread asks whether any nontrivial channel can be both amplitude-linear and density-only; the unconditional collapse says no, without feeding substrate access as a hypothesis.
proof idea
No proof body: this is a structure whose fields are propositions. Inhabitation is supplied downstream by packing five sibling results: universality of substrate access for amplitude-linear maps; the iff characterisation; the unconditional density-only vanishing lemma; the corresponding existential no-go; and the universal-witness calculation that id ⊗ L under canonical access induces exactly $L$. Each field is a direct assignment of the matching lemma; the structure itself only records the bundle interface.
why it matters
This is the master cert for the substrate-semantic unconditional closure of Gravity Track 2.C. The module status is theorem-level (zero sorry, zero RS-internal axiom): substrate access is forced by amplitude-linearity, so the access principle is derived rather than assumed, and the density-only no-go holds with no further access input.
Downstream, the concrete package substrateSemanticsUnconditionalCert fills every field, and substrateSemanticsUnconditionalCert_inhabited records nonemptiness. That package is the citation surface for the one-statement unconditional substrate-semantics theorem in the same module.
In the broader Recognition chain the result sits on the quantum-channel / gravity side of the eight-tick register (T7 octave), not on the J-uniqueness or dimension-forcing steps. It closes an internal load-bearing hypothesis rather than opening a new forcing landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.