module module high

`IndisputableMonolith.Foundation.LogicFromCost`

This module defines propositional configurations as a proposition paired with a balance ratio derived from pre-logical cost. Researchers formalizing the emergence of logic from Recognition Science cost minimization would cite it as the bridge between ontology predicates and logical stability. The module consists entirely of definitions that extend the Law of Existence and PreLogicalCost without any proofs.

claimA propositional configuration is a pair $(P, r)$ where $P$ is a proposition and $r > 0$ is its ratio, with $r = 1$ for perfect balance (true and stable), $r o 0$ for absence (false), and $r o \infty$ for unbounded instability.

background

The module imports LawOfExistence, which states that x exists if and only if defect(x) = 0. It imports OntologyPredicates, which define RSExists and RSTrue as selection outcomes from cost minimization under the unique J function. PreLogicalCost supplies configurations already constrained to the unit interval. The setting is the derivation of propositional notions directly from cost structures in Recognition Science.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the core objects for deriving logic from cost, feeding the framework's treatment of contradictions and consistency. It operationalizes the Law of Existence and OntologyPredicates to ground truth and stability in the J-cost function.

scope and limits

Does not contain theorems or proofs.
Does not define the J function or defect measures.
Does not address physical or numerical interpretations beyond propositional ratios.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.OntologyPredicates module_import
IndisputableMonolith.Foundation.PreLogicalCost module_import

declarations in this module (19)

structure PropConfig L70
def prop_cost L79
def IsStable L82
def IsUnstable L85
structure ContradictionConfig L100
def contradiction_cost L114
theorem contradiction_positive_cost L127
def IsLogicalContradiction L152
theorem logical_contradiction_impossible L162
theorem zero_cost_contradiction_forbidden L173
structure ConsistentConfig L182
def consistent_cost L191
theorem consistent_zero_cost_possible L197
theorem consistent_minimum_cost L204
theorem logic_from_cost L221
theorem why_logic_is_real L256
theorem prelogical_boolean_fragment L268
theorem mp_from_cost_and_logic L291
theorem logic_from_cost_summary L319