pith. sign in
module module high

IndisputableMonolith.Foundation.DiscretenessForcing

show as:
view Lean formalization →

The DiscretenessForcing module re-expresses the J-cost function in logarithmic coordinates as J(e^t) = cosh(t) - 1, a convex bowl centered at t = 0. Researchers formalizing the Recognition Science foundation cite it when moving from cost minimization to discrete ledger structures. The module supplies supporting definitions and lemmas on J_log properties that downstream modules import directly.

claim$J(e^t) = cosh(t) - 1$

background

The module resides in the Foundation layer and imports the Cost module together with LawOfExistence. The latter states that x exists if and only if defect(x) = 0. It introduces J_log as the J function rewritten in log coordinates, together with its immediate consequences such as non-negativity at zero, symmetry, and the absence of isolated zeros.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the log form of J required by InevitabilityStructure, LedgerForcing, OntologyPredicates, and PhiForcing. It supports the self-similarity argument that forces phi and the double-entry ledger structure. It also underpins the zero-composition interfaces used in the number-theory modules.

scope and limits

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (20)