t2_holds_eq_corollary
plain-language theorem explainer
Audit-grade equality: the standalone certificate that discreteness is forced coincides with the corollary obtained by routing the absolute-floor bridge through logic and the meta-principle. Chain auditors cite it to confirm a single canonical T2 surface rather than two parallel proofs. The argument is pure Subsingleton elimination on the shared proposition type.
Claim. The standalone certificate that discreteness is forced equals the composite obtained by applying the T2-from-T1 corollary to the T1-from-T0 corollary applied to the T0 surface built from the canonical absolute-floor (T-1) to T0 bridge.
background
The Unified Forcing Chain module shows that T0 through T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). In that ladder, T2 is discreteness: continuous configurations cannot stabilize under the cost, so admissible states are discrete.
Upstream, the canonical T-1 to T0 bridge packages the Boolean absolute floor, its floor configuration, recognition cost, and the work constraint with consistency at zero cost. From that bridge one builds the T0 surface (logic forced by cost minimization: consistency is cheap, contradiction expensive). T1 (the meta-principle that nothing has infinite cost) is then a corollary of T0, and T2 is a corollary of T1 via a state dichotomy on the discrete floor.
The standalone discreteness certificate and this routed composite both inhabit the same proposition. The present declaration records that they are definitionally the same object for audit purposes.
proof idea
Both sides of the equality are terms of the same proposition (the T2 discreteness surface). Lean treats that type as a subsingleton, so Subsingleton.elim identifies any two inhabitants. No algebraic unfolding of the corollaries is required; the proof is a one-line uniqueness argument on proof terms.
why it matters
In the Complete Inevitability Chain, every level from the absolute floor through T8 must be forced with no parallel ad-hoc certificates. This equality pins the standalone T2 surface to the unique path T-1 bridge → T0 (logic from cost) → T1 (meta-principle) → T2 (discreteness).
It is an audit seam rather than a new physical claim: it guarantees that later steps (ledger symmetry, unique J, φ, eight-tick octave, D=3) that consume discreteness are not silently depending on a second, inequivalent T2 proof. The module's stronger claim ("no gaps: every step is forced") relies on such equalities to keep the chain single-threaded. No downstream consumers are recorded yet; the value is local integrity of the forcing spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.