logic_from_cost_summary
plain-language theorem explainer
The theorem collects that consistent configurations reach zero cost exactly at ratio one while contradictions incur positive cost or reduce to the singular state where both ratios equal one, with the defect diverging at small ratios and vanishing at unity. Researchers tracing the emergence of logic in Recognition Science cite it to show cost minima select stable non-contradictory states. The proof is a term-mode conjunction that directly assembles six prior lemmas on defect behavior and consistency.
Claim. There exists a consistent configuration $c$ (a proposition asserted without its negation) such that its cost is zero, every consistent configuration has nonnegative cost, the cost of a consistent configuration is zero if and only if its ratio equals one, every contradiction configuration (asserting both a proposition and its negation) has positive cost or is a logical contradiction (both component ratios equal one), for every real number $C$ there exists an epsilon greater than zero such that the defect exceeds $C$ for all sufficiently small positive arguments, and the defect at unity is zero.
background
In this module a consistent configuration consists of a proposition together with a positive real ratio whose cost is the defect functional; a contradiction configuration asserts both a proposition and its negation with complementary ratios, and the logical contradiction predicate holds exactly when both ratios equal one. The defect is defined by defect x := J x, where J is the cost function J(x) = (x + x^{-1})/2 - 1. The local setting is the explicit bootstrapping inside classical logic: cost minima are shown to behave like logical consistency without deriving logic itself from cost.
proof idea
The proof is a term-mode construction of the six-way conjunction. It supplies consistent_zero_cost_possible for the existence clause, applies defect_nonneg to each consistent configuration via its ratio positivity, invokes defect_zero_iff_one for the equivalence, calls contradiction_positive_cost for the contradiction clause, uses nothing_cannot_exist for the divergence of defect near zero, and closes with defect_at_one.
why it matters
This summary closes the module by packaging the consequences of the J-cost landscape for logical structures, confirming that consistency is the minimum-cost state while contradictions are excluded by positive or infinite cost. It supports the Recognition Science thesis that logic emerges as the structure of cost minima rather than being imposed externally, aligning with the metalanguage scope that the cost landscape is the logical landscape. No downstream theorems are recorded, but the result fills the bridge from foundational cost to emergent logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.