T1_MP_Forced
plain-language theorem explainer
T1 packages the Meta-Principle as three cost statements on the Boolean floor: inconsistent configurations have strictly positive recognition-work cost, zero-cost states are consistent, and the marked inconsistent bit has positive cost. Anyone citing the T0–T1 step of the complete forcing chain uses this interface. It is a Prop-structure (definitional bundle), not an independent proof; the content is discharged as a corollary of T0.
Claim. T1 (Meta-Principle forced) is the proposition that, on the Boolean recognition-work floor with cost $C$: (i) every inconsistent configuration $\Gamma$ satisfies $C(\Gamma)>0$; (ii) $C(\Gamma)=0$ implies $\Gamma$ is consistent; (iii) the marked inconsistent Boolean state has $C(\mathsf{true})>0$. Equivalently: an inconsistent recognition-work state cannot be selected at zero cost.
background
The Unified Forcing Chain module claims that T−1 through T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration), rather than merely compatible with it. T0 already asserts that classical logic on the Boolean floor emerges from cost minimization: consistency is the cheap (zero-cost) locus.
A configuration space supplies an empty config, a join, and a consistency predicate IsConsistent. On the absolute-floor Boolean model, recognition-work cost $C$ is the Boolean specialization of the distinction-derived cost. Upstream, total recognition cost is a sum of ratio weights (doubled $J$-cost), and observer/event cost is the $J$-cost of the event state; non-negativity of $J$ is the ambient positivity background.
T1 is the Meta-Principle layer in the chain sketch: MP ← cost (nothing inconsistent is free). The doc-comment states the slogan directly: an inconsistent recognition-work state cannot be selected as a zero-cost state. The structure is explicitly marked as a corollary surface of T0, not a sibling axiom.
proof idea
There is no proof body: this declaration is a structure ... : Prop that bundles three fields. inconsistent_positive and zero_cost_consistent are the two directions of the cost/consistency split on Bool; marked_inconsistent_positive pins the concrete inconsistent witness true to strictly positive cost.
Inhabitants are built downstream by t1_corollary_of_t0 from a T0_Logic_Forced witness, and the bridge certificate T0_To_T1_Bridge records definitional equality t1 = t1_corollary_of_t0 h0. The mathematical work is therefore inherited from T0’s identification of zero cost with consistency and positivity on inconsistent floor states; T1 only names that payload as the Meta-Principle interface.
why it matters
In the forcing ladder, T1 is the MP step between T0 (logic from cost) and T2 (discreteness). Downstream, CompleteForcingChain and CompleteForcingChainT8 both carry a t1 : T1_MP_Forced field; T0_To_T1_Bridge certifies that this field is exactly the T0 corollary, and T1_To_T2_Bridge / t1_to_t2_bridge_holds consume a T1 witness to open the discreteness bridge on the Boolean floor.
Framework-wise this is the first post-logic inevitability in the primer chain (before T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). It encodes that selection at zero recognition-work cost cannot land on inconsistency—the cost-theoretic stand-in for “ex falso / MP is forced,” without treating MP as a free logical postulate. The honesty note on the T8 complete chain still applies higher up (T5 uniqueness does not secretly depend on the floor), but T1 itself is the clean T0→T1 link the bridges re-export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.