logic_from_cost
plain-language theorem explainer
Logic emerges as the minimum-cost configurations in the Recognition Science cost landscape. Foundational physicists would cite it to derive that stable reality must be logically consistent without external imposition. The proof is a term-mode conjunction that packages existence of a zero-cost consistent configuration, nonnegativity of consistent cost, its equivalence to ratio one, and positive cost for contradictions.
Claim. There exists a consistent configuration $c$ (a proposition $P$ asserted without its negation, equipped with positive real ratio) such that its cost is zero; for every consistent configuration $c$ the cost is nonnegative and equals zero precisely when the ratio equals one; and for every contradiction configuration $c$ (asserting both $P$ and its negation with positive ratios) the cost is positive or both ratios equal one.
background
A ConsistentConfig is a structure carrying a proposition $P$ and positive real ratio, representing an assertion of $P$ without its negation; it can reach zero cost. A ContradictionConfig carries both $P$ and its negation together with complementary positive ratios; IsLogicalContradiction holds exactly when both ratios equal one. The cost functions consistent_cost and contradiction_cost are defined via the underlying defect measure on these ratios.
proof idea
The proof is a term-mode construction that directly builds the four-way conjunction: consistent_zero_cost_possible supplies the existence of a zero-cost consistent configuration; the lambda applying defect_nonneg to the ratio positivity hypothesis gives nonnegativity; the lambda applying defect_zero_iff_one gives the ratio-equivalence; and contradiction_positive_cost closes the clause for contradiction configurations.
why it matters
This is the main theorem of the LogicFromCost module, establishing that logical consistency is the structure of cost minimization. It shows contradictions cannot stabilize while consistent configurations can reach zero defect, grounding the claim that logic is the geometry of the cost landscape minima. The result closes the bridge from the J-cost functional to the emergence of logic, supporting the economic interpretation that reality equals what minimizes defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.