t4_holds_eq_corollary
plain-language theorem explainer
Audit-grade equality: the standalone certificate that T4 (recognition) holds is identical to the T4 corollary fed by the fully routed T2 and T3 surfaces from the absolute-floor bridge. Chain auditors cite it to rule out a second, untracked T4 witness. The proof is one-line subsingleton elimination on the T4 theorem surface.
Claim. The standalone proof that recognition is forced equals the T4 corollary applied to (i) discreteness forced from the meta-principle routed out of logic-from-cost via the absolute-floor bridge, and (ii) the ledger forced from that same logic surface together with discreteness.
background
The module UnifiedForcingChain claims a complete inevitability ladder from an absolute floor through T0–T8, all driven by the Recognition Composition Law plus normalization and calibration. In that ladder, T4 is the recognition step: once a cost-symmetric ledger exists and observables are available, recognition events are forced.
Upstream, the absolute-floor bridge supplies a normalized Boolean floor; t0_from_tminus1_to_t0_bridge turns it into the T0 (logic-from-cost) surface. T1 (meta-principle: nothing has infinite cost) is a corollary of T0; T2 (discreteness) is a corollary of T1; T3 (ledger, via $J(x)=J(1/x)$ symmetry) is a corollary of T0 and T2. The T4 corollary then consumes those T2 and T3 certificates.
This declaration does not re-prove T4. It equates the named standalone t4_holds inhabitant with that fully expanded corollary spine, so the audit graph has a single T4 surface.
proof idea
Both sides of the equality are terms of the same T4 theorem-surface type. That type is a subsingleton (at most one inhabitant up to equality), so Subsingleton.elim identifies the standalone t4_holds with the composite
t4_corollary_of_t2_t3 applied to the routed T2 certificate (t2_corollary_of_t1 of t1_corollary_of_t0 of the bridge-built T0) and the routed T3 certificate (t3_corollary_of_t0_t2 of the same T0 and T2). No algebraic content is re-derived; the proof is pure proof-irrelevance on the T4 surface.
why it matters
In the Complete Inevitability Chain, T4 is the hinge from ledger structure to recognition events, sitting just before T5 (unique $J$), T6 ($\varphi$ forced), T7 (eight-tick octave), and T8 ($D=3$). The module’s stronger claim is that every level is forced, not merely compatible; audit-grade equalities like this one pin the standalone T4 certificate to the unique routed spine from T-1, so later steps cannot silently depend on a different recognition witness.
No downstream declarations currently list this equality as a dependency. Its role is documentary and machine-checkable hygiene inside Foundation.UnifiedForcingChain: anyone reading the forcing graph can see that t4_holds is not an alternate construction. It closes a potential gap between “T4 is proved somewhere” and “T4 is exactly the corollary of the T2/T3 surfaces already on the chain.”
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.