canonicalCyclicJointOperator_arisesFromRecognitionProbe
plain-language theorem explainer
The canonical cyclic joint operator on the eight-tick joint substrate, paired with the recognition update as channel response, arises from recognition-probe substrate access. Anyone citing the substrate-locality principle as non-vacuous needs this witness. The proof applies the pure-tensor factorization route with the constant-one matter reference and channel index zero, then checks the calibration coordinate is nonzero via one ≠ zero.
Claim. The canonical cyclic joint operator $R_J^{\mathrm{cyc}}$ on $\mathrm{Signal}_8 \otimes \mathrm{Signal}_8$, together with the recognition update $R_C$ (projector-after-shift on the recognition sector), satisfies the substrate-access principle: there exist access data such that $R_C$ equals the induced channel harvested from $R_J^{\mathrm{cyc}}$ by fixing a matter reference state, applying $R_J^{\mathrm{cyc}}$ once, and reading a calibrated channel coordinate.
background
This module (Gravity Track 2.C) closes the substrate locality / measurement-access principle. Operational channel observables on the joint substrate $\mathrm{Signal}_8 \otimes \mathrm{Signal}8$ are obtained as recognition probes: fix a matter reference $\psi_0$, run the joint linear operator $R_J$ once, and read a channel coordinate $i_0$ normalised by a calibration scalar $\chi \neq 0$. The induced channel is then $R_C\varphi = \chi^{-1}\cdot\mathrm{extractSecond}{i_0}(R_J(\mathrm{insertFirst},\psi_0,\varphi))$, which is automatically a joint section readout.
ArisesFromSubstrateAccess is the per-channel proposition that $R_C$ equals the induced channel for some such access data. The recognition update itself is the concrete projector-after-shift map on the eight-tick register. Session 111 already forced amplitude-linearity from nonzero section readout; the remaining step was to derive section readout from substrate locality rather than assume it.
The canonical cyclic joint operator is the Session-87 recognition-coupled pure tensor of cyclic shifts. The present result shows that this operator, with recognition update as channel response, inhabits the substrate-access proposition.
proof idea
Term-mode proof via the pure-tensor route. Apply arisesFromSubstrateAccess_of_pureTensorFactorization to the known pure-tensor factorization of the canonical cyclic joint operator, taking matter reference $\psi_0 = 1$ (the constant-one eight-tick signal) and channel index $i_0 = 0$.
The remaining obligation is that the recognition update of $1$, evaluated at coordinate $0$, is a nonzero complex. Unfolding the projector-after-shift definition reduces this to the statement that the constant-one signal at the shifted index is nonzero, discharged by one_ne_zero.
why it matters
This is the non-vacuous inhabitant that makes the Session-113 substrate-locality principle live rather than empty. Downstream, canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate quotes it directly: the canonical T0–T8 joint dynamics admits the recognition probe as substrate access, and the operational channel response is the recognition update, already known to be amplitude-linear.
It also feeds the master certificate substrateLocalAccessCert and the one-statement theorem substrate_local_access_one_statement, which packages the full chain
ArisesFromSubstrateAccess → JointSectionReadout → IsAmplitudeLinear
together with the density-only no-go. Under substrate locality, section readout (Session 111) is no longer an assumption; it is the definition of how the operational channel is harvested from $R_J$.
Framework landmarks: the eight-tick octave (T7) supplies the $\mathrm{Signal}_8$ register; the T0–T8 forcing chain supplies the canonical cyclic joint dynamics being witnessed. The factor-product theorem (Sessions 85–88) becomes a corollary of the same chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.