T1_MP_Forced
plain-language theorem explainer
Public alias for the T1 meta-principle: an inconsistent recognition-work state on the Boolean floor cannot be selected at zero cost. Anyone assembling the T−1–T8 forcing spine cites this surface rather than the private bridge module. The declaration is a pure abbrev re-export with no extra proof obligation.
Claim. The T1 meta-principle is the proposition that (i) every inconsistent Boolean floor configuration has strictly positive recognition-work cost, (ii) every zero-cost Boolean configuration is consistent, and (iii) the marked inconsistent state has positive cost. This public name is definitionally identical to that proposition as packaged on the T−1-to-T1 bridge.
background
The module exposes the public, theory-only T−1 through T8 forcing spine and stops before private operator or measurement layers. In that spine, T−1 is the absolute distinguishability floor, T0 is the Boolean recognition-work split (logic from cost), and T1 is the cost-form meta-principle.
Upstream, the T−1-to-T1 bridge packages T1 as a structure with three fields: inconsistent states have positive Boolean recognition cost; zero cost implies consistency; and the marked inconsistent Boolean has positive cost. The unified forcing chain records the same content as a corollary of T0: "an inconsistent recognition-work state cannot be selected as a zero-cost state."
Recognition cost here is the Boolean floor cost functional from the T−1/T0 layer; consistency is the ConfigSpace predicate that marks which floor states are admissible.
proof idea
No proof body. The declaration is a one-line abbrev that definitionally equals TMinus1ToT1Bridge.T1_MetaPrinciple_Forced. All mathematical content and any later witnesses live on that upstream structure (or on the parallel UnifiedForcingChain T1 surface used as a corollary of T0).
why it matters
T1 is the first cost-form meta-principle in the Recognition forcing chain: inconsistent recognition work is never free. This public alias is the t1 field of CompleteForcingChainT8 and feeds T1_To_T2_Bridge / t1_to_t2_bridge_holds, which open the path to two-state discreteness (T2), ledger bookkeeping (T3), and onward through J-uniqueness (T5), φ (T6), the eight-tick octave (T7), and D = 3 (T8).
On the unified chain it appears in CompleteForcingChain, T0_To_T1_Bridge, and t1_corollary_of_t0, which stress that T1 is not an independent sibling of T0 but the direct corollary of the T0 cost/consistency split. Citing this abbrev keeps consumer code on the public spine rather than private bridge internals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.