pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.JCostCoshIdentity

show as:
view Lean formalization →

The JCostCoshIdentity module establishes the core identity J(e^y) = cosh(y) - 1 for the recognition cost function. Physicists and mathematicians tracing the forcing chain cite these lemmas when converting exponential costs into hyperbolic form for ladder calculations. The module supplies the identity together with immediate corollaries on zero value, symmetry, and positivity, all obtained by direct substitution into the base definition imported from Cost.

claim$J(e^y) = (e^y + e^{-y})/2 - 1 = cosh(y) - 1$

background

Recognition Science defines the J-cost via the functional equation J(x) = (x + x^{-1})/2 - 1. The present module works entirely inside the exponential parametrization x = e^y, converting the expression into the standard hyperbolic identity. It imports the Cost module, which supplies the primitive J definition and the Recognition Composition Law used in later steps of the T0-T8 chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the hyperbolic representation required by T5 (J-uniqueness) in the unified forcing chain. It feeds downstream results that express mass rungs and Berry thresholds in terms of cosh and phi-ladder quantities.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)