t4_holds
plain-language theorem explainer
Recognition is forced on the pre-analytic Boolean floor: a non-trivial discrete distinction already yields a recognition witness and relation before any analytic J-cost is imposed. Citers of the T0–T8 inevitability chain and the gravity master theorem need this step. The proof is pure bridge composition from the absolute floor through T0–T3, then the T2+T3→T4 bridge.
Claim. The recognition-forcing claim holds on the pre-analytic floor: the normalized two-point Boolean recognition floor (with the Boolean recognition cost and the identity equivalence) is non-trivial ($\exists a,b:\mathrm{Bool},\, a\neq b$), admits a recognition witness $\mathrm{Recognize}(\mathrm{Bool},\mathrm{Bool})$, and carries a recognition structure on the Boolean carrier. Richer observable/$J$-stability is deferred to an analytic refinement.
background
The module UnifiedForcingChain assembles the complete inevitability chain: every level T-1 through T8 is forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$), not merely shown compatible. In that ladder, T4 is the recognition step: ledger plus observables force a recognition witness on the discrete carrier.
T4_Recognition_Forced packages four floor-level facts: a normalized two-point recognition floor on Bool with the Boolean recognition cost; existence of a non-trivial distinction; non-emptiness of Recognition.Recognize Bool Bool; and a recognition structure on that carrier. The doc keeps the richer observable/$J$-stability theorem as an analytic refinement, so this surface is deliberately pre-analytic.
Upstream bridges supply the inputs. The canonical T-1→T0 bridge installs the absolute Boolean floor, floor config, and recognition-work constraint. T0→T1, T1→T2, and T0+T2→T3 bridges then deliver logic, discreteness, and the ledger surface that T4 consumes.
proof idea
Term-mode chain of bridge projections, no new algebra.
Start from tminus1_to_t0_bridge_holds (canonical absolute-floor bridge). Project T0 via t0_from_tminus1_to_t0_bridge. Feed that into t0_to_t1_bridge_holds and take .t1. With the T-1→T0 bridge and T1, apply t1_to_t2_bridge_holds and take .t2. With bridge, T0, and T2, apply t0_t2_to_t3_bridge_holds and take .t3. Finally apply t2_t3_to_t4_bridge_holds to the T2 and T3 surfaces and project .t4, which is exactly T4_Recognition_Forced.
Each step is a theorem-backed bridge already proved elsewhere; this declaration only routes them in order.
why it matters
T4 is the recognition rung in the forcing chain (module diagram: T4 ← Ledger + observables). Without it the chain stops at a discrete ledger with no recognition witness, and later φ-forcing, eight-tick, and D=3 steps have nothing to recognize against.
Downstream, T0_T8_holds_proven in Gravity.MasterTheorem packages t4_holds with t0–t3 and t5–t8 as the single master fact that the full T0–T8 surface is proved. The sibling t4_holds_eq_corollary gives an audit-grade equality: the standalone theorem equals the corollary applied to the routed T2 and T3 surfaces, so the two presentation paths cannot drift.
In framework terms this closes the pre-analytic half of the chain before T5 (unique J from d'Alembert + normalization + calibration). It does not yet pin J, φ, the eight-tick octave, or D=3; those are later rungs that cite this surface only indirectly through the master package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.