PhysicalOperatorCompatibility
plain-language theorem explainer
Certificate that a recognition operator agrees with the forced quarter-turn shift law on the odd DFT core of the eight-tick carrier. Model builders who attach a physical operator to the T0–T8 spine cite it so the operator is not an unconstrained sibling of the chain. It is a one-field Prop structure; the companion theorem discharges it from the bridge’s universal shift law.
Claim. Fix a T7/T8-to-operator-core bridge and a recognition operator $R$. Compatibility holds when, for every eight-tick signal $f$ in the quarter-turn core (the $\mathbb{C}$-span of the odd DFT-8 modes), the evolution $R\cdot f$ equals the bare cyclic shift of $f$ on the register $\mathrm{Fin}\,8\to\mathbb{C}$.
background
The Unified Forcing Chain module treats T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T7 forces the eight-tick octave ($2^3$); T8 forces $D=3$. Their operator-core bridge packages the canonical carrier $\mathrm{Signal8}=\mathrm{Fin},8\to\mathbb{C}$, complexification of the DFT-8 shift, and the fact that the odd-mode quarter-turn core is neutral under that shift.
The cyclic shift advances the reading index by one tick: $(Tf)(k)=f(k+1\bmod 8)$. The quarter-turn core is the span of DFT modes with odd index; the bridge proves every recognition operator preserves this core by bare shift. A recognition operator is the discrete evolution map on that carrier used when the mathematical spine is packaged as a physical model.
This structure does not add new dynamics. It records the single agreement condition the physical layer must meet with the already-forced operator core.
proof idea
Definitional Prop structure, not a proved theorem. One field, evolves_as_shift_on_core, asserts pointwise equality of $R$'s evolution with the spectral cyclic shift on every vector of the quarter-turn core. No tactics or lemmas live in the structure body. The companion theorem builds an instance by applying the bridge field that every operator preserves the core under shift, so any plugged-in $R$ inherits compatibility automatically.
why it matters
Closes the hand-off from the unconditional T0–T8 spine to the physical model layer. Downstream, PhysicalForcingChain extends the complete forcing chain by a recognition operator together with this compatibility certificate; the doc states the physical model is derived from the mathematical chain, not the reverse. The automatic instance theorem shows every recognition operator satisfies the certificate via the bridge’s universal shift law, so physical packaging cannot smuggle in a free evolution on the core.
In framework terms this sits after T7 (eight-tick octave) and T8 ($D=3$), where the operator core and complex structure are already forced. It keeps the physical operator aligned with the same quarter-turn dynamics the chain derives, rather than treating dynamics as an extra axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.