pith. sign in
def

Jcost

definition
show as:
module
IndisputableMonolith.Cost
domain
Cost
line
6 · github
papers citing
62 papers (below)

plain-language theorem explainer

The Jcost definition supplies the explicit formula for the recognition cost function J(x) = (x + x^{-1})/2 - 1 on the reals. Researchers in Recognition Science cite this as the base cost measure satisfying the composition law and fixed-point conditions from the forcing chain. The declaration is introduced directly as a noncomputable definition with no proof body or additional obligations.

Claim. The cost function is defined by $J(x) := (x + x^{-1})/2 - 1$ for $x : ℝ$.

background

Recognition Science derives all physics from one functional equation whose T5 step isolates a unique cost function J. The Cost module opens with this definition to encode the recognition cost of a scale factor x. It matches the closed form J(x) = cosh(log x) - 1 and serves as the starting point for all subsequent cost identities in the module.

proof idea

The definition is supplied directly by the algebraic expression (x + x^{-1})/2 - 1, matching the closed form required by J-uniqueness in the forcing chain.

why it matters

This definition anchors cost calculations throughout the Recognition framework and corresponds to the T5 J-uniqueness landmark in the unified forcing chain. It feeds the Recognition Composition Law and the derivations of constants such as alpha^{-1} in (137.030, 137.039). The module's sibling results on nonnegativity, symmetry, and exponential agreement all rest on this base expression.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 62)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.