T0_AnalyticCost_Refinement
plain-language theorem explainer
Bundles three analytic cost properties that refine T0 once the closed-form reciprocal cost is available: some consistent configuration has cost zero, every contradiction is either strictly positive-cost or a classical logical contradiction, and consistent costs are nonnegative. Forcing-chain authors cite it to keep the old LogicFromCost surface as a downstream refinement without loading the pre-analytic chain with J. Pure Prop structure; no proof body.
Claim. There exists a consistent configuration $c$ (a proposition $P$ with positive ratio, no $\neg P$ asserted) such that its defect cost is $0$. For every contradiction configuration (both $P$ and $\neg P$ asserted, with ratios $r_P$ and $r_{\neg P}$), the sum of defects is $>0$, or else both ratios equal $1$ (a logical contradiction state). Every consistent configuration has nonnegative defect cost.
background
The Unified Forcing Chain module aims to force T-1 through T8 from the cost foundation (Recognition Composition Law plus normalization and calibration). T0 is the logic step: consistency is cheap under cost minimization, so classical logic emerges rather than being assumed.
Upstream, LogicFromCost packages configurations. A consistent configuration carries a single proposition $P$ and a positive real ratio; its cost is the defect of that ratio, which can vanish at ratio $1$. A contradiction configuration asserts both $P$ and $\neg P$ with complementary ratios; total cost is the sum of the two defects. When both ratios equal $1$, one has a logical contradiction state (classically impossible).
This structure is the analytic refinement of that T0 surface after the canonical reciprocal cost $J$ is on hand. It deliberately keeps the pre-analytic chain free of the closed-form $J$, recording only the cost inequalities the old payload already stated.
proof idea
Definitional Prop structure with three fields and no proof body. Inhabitants are assembled by supplying the three named LogicFromCost facts: existence of a zero-cost consistent configuration, the dichotomy that every contradiction has positive cost or is a logical contradiction, and nonnegativity of defect on consistent ratios. The companion theorem t0_analytic_refinement_holds fills those fields from consistent_zero_cost_possible, contradiction_positive_cost, and defect_nonneg.
why it matters
Keeps the historical analytic T0 interface alive inside the Complete Inevitability Chain without making early steps depend on the closed-form $J(x)=(x+x^{-1})/2-1$. Downstream, t0_analytic_refinement_holds certifies the structure, and T5_To_AnalyticRefinements_Bridge consumes it among the analytic refinements that rest on unique $J$ after T5 (J-uniqueness in the forcing chain). That bridge records that the five analytic-refinement surfaces share the reciprocal cost forced by T5, so this bundle is the T0 endpoint of that post-uniqueness cleanup. Framework landmark: T0 (logic from cost minimization) in the T-1..T8 ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.