PhysicalForcingChain
plain-language theorem explainer
Packages the complete T−1 through T8 forcing spine with a physical recognition operator that must obey the quarter-turn core shift law. Physicists cite it when lifting the unconditional mathematical chain into a concrete dynamical model. It is a structure extension: inherit CompleteForcingChain, add a trivial H witness, an operator R, and a compatibility certificate.
Claim. A physical forcing chain is a complete forcing chain (absolute floor through $T8$, with all internal bridges) together with a recognition operator $R$ that is compatible with the $T7$–$T8$ operator-core bridge: on every eight-tick signal in the quarter-turn core, $R$ evolves by the bare cyclic shift. An auxiliary trivial witness $H:\mathrm{True}$ is carried for packaging.
background
The module UnifiedForcingChain proves that levels T−1 through T8 are forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). The complete chain structure bundles the absolute floor, logic-from-cost, Meta-Principle, discreteness, ledger, recognition, unique $J$, $\varphi$, eight-tick octave, and $D=3$, plus bridges into operator, Hamiltonian, and measurement layers.
CompleteForcingChain is that full spine. The physical layer sits on top: a RecognitionOperator is not free-floating. Compatibility means that on the quarter-turn core of eight-tick signals, evolution equals the spectral cyclic shift already forced by the T7–T8 operator-core bridge. The shifted cost $H(x)=J(x)+1$ (d'Alembert form of RCL) underpins uniqueness of $J$ upstream; here $H:\mathrm{True}$ is only a packaging slot, not that cost functional.
Doc-comment stance: physics is derived from the math chain, not the reverse.
proof idea
No proof body: this is a structure definition. It extends CompleteForcingChain by three fields: a trivial True witness, a RecognitionOperator $R$, and a PhysicalOperatorCompatibility certificate relative to the chain's t7_t8_to_operator bridge. That certificate is the single Prop field evolves_as_shift_on_core: for every $f$ in the quarter-turn core, $R.\mathrm{evolve}, f$ equals cyclic shift. Instantiation is deferred to the downstream constructor physical_forcing_chain, which fills the base via complete_forcing_chain and supplies compatibility from the bridge.
why it matters
Closes the packaging step from "Complete Inevitability Chain" (T−1…T8 forced from cost) to a usable physical model object. Downstream, physical_forcing_chain builds an inhabitant: same unconditional spine, plus any $R$ certified against the operator-core bridge. That keeps physical dynamics from becoming an unconstrained sibling of the forcing results.
Framework landmarks: T5 unique $J$ (and RCL/$H$), T6 $\varphi$, T7 eight-tick ($2^3$), T8 $D=3$ all sit inside the extended base; the new content is only operator agreement with the quarter-turn core. Supports the module claim that constants and dynamics are read off the forced chain rather than postulated beside it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.