T0_Logic_Forced
plain-language theorem explainer
T0 packages classical logic as the zero/positive split of recognition work on the Boolean configuration floor. Anyone citing the opening of the forcing chain (absolute floor through Meta-Principle) uses this Prop-structure as the T0 interface. Five fields bundle a recognition-work certificate, zero cost on the consistent Boolean, positive cost on inconsistency, the converse dichotomy, and independent additivity. It is a definitional interface, not a proved theorem.
Claim. The T0 interface is the proposition that (i) a recognition-work constraint certificate exists on the Boolean configuration space, (ii) the Boolean recognition cost of $\mathsf{false}$ is $0$, (iii) every inconsistent Boolean has strictly positive cost, (iv) zero cost implies consistency, and (v) cost is additive under join of independent Booleans.
background
This module isolates the first three levels of the forcing chain without importing the analytic $J$-cost surface: T-1 (absolute floor of distinguishability), T0 (minimal recognition-work cost interface), and T1 (cost-form Meta-Principle: inconsistent floor states cannot be selected at zero cost).
A configuration space supplies an empty configuration, a binary join, a consistency predicate, and an independence relation (no shared predicates), with join a commutative monoid. A cost function $C$ on that space obeys dichotomy (zero cost iff consistent) and independent additivity. The master certificate RecognitionWorkConstraintCert bundles a cost function with emp-zero and the recognition-work consequences above pure distinguishability algebra.
On the Boolean floor the concrete cost is $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$. T0 is exactly the statement that this Boolean recognition-work split satisfies the five interface fields above.
proof idea
No proof body: this is a Prop-structure (definitional interface). The five fields are the mathematical content of T0. Inhabitation is supplied downstream by t0_holds, which fills recognition_work from the Boolean recognition-work certificate, takes consistency-zero by reflexivity on the concrete cost, and obtains the positive/zero dichotomy directions from the cost-function lemma that positive cost is equivalent to inconsistency, together with independent additivity from the Boolean cost definition.
why it matters
T0 is the second rung of the public T-1 to T1 bridge and the logical entry point of the larger forcing chain toward T8. Downstream, t0_holds asserts the interface is realized on the Boolean floor; t1_corollary_of_t0 derives T1 (inconsistent states cannot be zero-cost selected) directly from the positive-cost and zero-cost-consistent fields; T0_To_T1_Bridge and t0_to_t1_bridge_holds package that corollary; TMinus1_To_T0_Bridge and TMinus1ToT1Cert chain the absolute floor through T0 into T1. The T-1-to-T8 spine reuses the same interface inside CompleteForcingChainT8. In framework terms this is the pre-analytic content of T0 before J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.