t0_from_tminus1
plain-language theorem explainer
From the absolute floor (meta-language proposition distinguishability plus a non-singleton universe), classical logic is forced as the zero/positive split of Boolean recognition work. Anyone assembling the Unified Forcing Chain cites this to enter T0 from T-1 with no extra axioms. The proof is a one-line projection of the T-1 to T0 bridge certificate.
Claim. Given an absolute-floor certificate (meta-language proposition distinguishability together with a non-singleton universe of discourse), logic is forced: the minimal Boolean configuration space carries a recognition-work cost under which every consistent state has cost $0$ and every inconsistent state has strictly positive cost.
background
The Unified Forcing Chain module proves that T0 through T8 are forced inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). The chain bottoms at T-1, the absolute floor: two preconditions of statability itself, namely meta-language proposition distinguishability and a non-singleton universe of discourse. That floor sits strictly below the Law of Logic.
T0 asserts that logic is not a pre-given structure. At the pre-analytic floor, logic is the zero/positive split of recognition work: consistent configurations have zero cost and inconsistent configurations have positive cost. Concretely, a Boolean floor witness from absolute-floor closure supplies a recognition-cost function on Bool with those sign properties.
Upstream, the bridge theorem packages any absolute-floor certificate into a T-1 to T0 bridge record carrying the Boolean floor configuration and its recognition cost. Its documentation states that "the absolute floor supplies the minimal T0 cost interface."
proof idea
One-line term proof. Apply the bridge theorem that turns an absolute-floor certificate into a T-1 to T0 bridge record, then project that record's T0 field. Recognition-work nonemptiness, zero cost on the consistent Boolean state, and strict positivity on inconsistent states are already discharged inside the bridge construction; nothing further is proved here.
why it matters
This is the entry step of the Complete Inevitability Chain: T-1 forces T0. The module's stronger claim over prior CPM closure is that logic itself emerges from cost minimization ("consistency is cheap"), rather than being assumed as a background calculus. From here the chain continues through the Meta-Principle (T1), discreteness (T2), ledger symmetry (T3), recognition (T4), unique J via d'Alembert (T5), self-similar $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). No downstream used_by edges are recorded on this surface yet; sibling surfaces such as the bare T0-holds certificate and the analytic-cost refinement sit on the same T0 structure and consume the same forced logic interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.