pith. sign in
module module high

IndisputableMonolith.Foundation.DiscretenessForcing

show as:
view Lean formalization →

The DiscretenessForcing module introduces the logarithmic form of the J-cost function as J(e^t) = cosh(t) - 1, a convex bowl minimized at t=0. Researchers tracing the Recognition Science forcing chain from cost minimization to discrete ledger structure cite these lemmas when shifting from multiplicative to additive variables. The module consists of direct definitions and elementary real-analysis properties.

claim$J(e^t) = J(e^{-t}) = J(e^t) + J(e^{-t}) + 2J(e^t)J(e^{-t})$, with $J(e^t) = J(e^{-t}) = 2J(e^{t/2})^2 + 2J(e^{t/2})$ and $J(e^t) = 0$ iff $t=0$.

background

The module imports the Cost framework (where J satisfies the Recognition Composition Law) and LawOfExistence, which states that x exists if and only if defect(x) = 0. It re-expresses the J-cost in logarithmic coordinates to support analysis of discrete structures. The module doc-comment states: J in log coordinates: J(eᵗ) = cosh(t) - 1. This is a convex bowl centered at t = 0.

proof idea

This is a definition module, no proofs. It defines J_log(t) := cosh(t) - 1 together with supporting lemmas on non-negativity, symmetry, quadratic bounds, and equivalence to the exponential form of J.

why it matters in Recognition Science

This module supplies the log-coordinate representation of J required by downstream modules including PhiForcing (self-similar discrete ledger forces phi), LedgerForcing (J-symmetry forces double-entry structure), OntologyPredicates (existence as cost-minimization outcome), and InevitabilityStructure. It supports the transition toward the eight-tick octave and D=3 in the T0-T8 forcing chain.

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)