canonicalAccess
plain-language theorem explainer
Canonical substrate-access datum: constant-1 matter probe on the eight-tick signal space, channel index 0, calibration 1. Anyone proving that amplitude-linear channels arise from substrate-internal joint operators cites this as the fixed recognition probe. It is a structure instance; the only proof obligation is χ ≠ 0, discharged by Peano one ≠ zero.
Claim. The canonical substrate-access datum is the triple $(\psi_0, i_0, \chi)$ with matter probe $\psi_0 = 1$ (the constant unit signal on the eight-tick space), channel coordinate $i_0 = 0$, and calibration $\chi = 1$, together with the witness $\chi \neq 0$.
background
Track 2.C studies operational recognition observables on the joint substrate: channel responses $R_C$ on the eight-tick signal space Signal8 (the $2^3$ period forced at $D=3$). An amplitude-linear channel is one witnessed by a $\mathbb{C}$-linear map $L$ on that space. Substrate access means: prepare a matter probe $\psi_0$, apply a joint linear operator once, read a channel coordinate $i_0$ with nonzero calibration $\chi$, and recover $R_C$ as the induced channel.
SubstrateAccessData packages exactly those three parameters plus the nonvanishing proof for $\chi$. This definition fixes the standard choice used throughout the unconditional closure: unit probe, zeroth coordinate, unit calibration. The nonvanishing fact is the elementary Peano inequality $1 \neq 0$ from the primitive recognition calculus.
The module's goal is to retire the substrate-locality / measurement-access principle as an independent hypothesis: every amplitude-linear $R_C$ must arise from some joint operator under this (or equivalent) access.
proof idea
Pure structure instance. Fields are set to the constant unit signal, index $0$, and calibration $1$. The sole proof field $\chi \neq 0$ is filled by the imported Peano lemma one_ne_zero. No further rewriting or case analysis.
why it matters
This is the fixed recognition probe that makes substrate access universal. Downstream, universalSubstrateAccessOperator_inducedChannel shows that the joint operator $\mathrm{id} \otimes L$ induces exactly the witness map $L$ under this access. That calculation feeds arisesFromSubstrateAccess_of_isAmplitudeLinear: every amplitude-linear channel arises from substrate access of the universal operator paired with this datum.
Those facts populate the master certificate SubstrateSemanticsUnconditionalCert and the one-statement theorem equating amplitude-linearity with existence of a substrate-access witness. In the Track 2.C chain, the substrate-access hypothesis is thereby derived rather than assumed, closing the unconditional substrate-semantics thread (Session 125). The eight-tick signal space is the T7 octave forced with $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.