t0_holds_eq_routed
plain-language theorem explainer
The direct global T0 theorem (logic forced by cost minimization) and the T0 surface obtained by routing through the absolute-floor bridge are the same proposition. Chain authors can cite either surface without changing theorem content. The proof is a one-line appeal to proof irrelevance on Prop.
Claim. The direct statement that T0 holds is equal, as a proposition, to the statement obtained by applying the absolute-floor-to-T0 bridge map to the established bridge theorem. In other words, the global T0 surface and the routed T0 surface carry identical proposition-level content.
background
The module UnifiedForcingChain assembles the complete inevitability ladder from the cost foundation (Recognition Composition Law plus normalization and calibration). The ladder begins at T-1 (absolute floor: meta-language Prop distinction in a non-singleton universe) and climbs through T0–T8. T0 is the claim that classical logic is forced by cost minimization: consistency is the cheap state, so inconsistent recognition-work configurations cannot be zero-cost selectable states.
Two presentation surfaces for T0 appear in the development. One is the direct global theorem that T0 holds. The other is a routed construction: start from the absolute-floor theorem, apply an explicit T-1-to-T0 bridge, and obtain a T0 witness. The present declaration equates those two surfaces at the level of propositions.
Upstream material supplies the cost and recognition primitives (J-cost on recognition events, derived costs of multiplicative recognizers, canonical arithmetic and measure objects) that make the T0 statement well-formed, but the equality itself does not re-open those constructions.
proof idea
Both sides inhabit the same proposition (the T0 theorem type). In Lean, every proposition is a subsingleton, so any two of its inhabitants are equal. The proof is the single term Subsingleton.elim _ _, which discharges the equality by proof irrelevance. No algebraic unfolding of the bridge or of the cost axioms is required.
why it matters
In the Recognition Science forcing chain, T0 is the first physics-facing step after the absolute floor: logic emerges from cost rather than being assumed. Maintaining two entry points (direct global vs. routed from T-1) is useful for different readers, but only if they are known to state the same theorem. This declaration records that coherence.
It sits inside the module’s stronger claim that every level T-1 through T8 is forced from the RCL axiom bundle, with no compatibility gaps. Downstream use is presently empty in the graph; the lemma is bookkeeping for the chain’s internal hygiene rather than a stepping stone to a named parent. It does not itself advance T5 (unique J), T6 (φ), T7 (eight-tick), or T8 (D=3), but it keeps the T0 surface unambiguous before those steps are cited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.