Jcost
Jcost supplies the explicit formula for the central cost function in Recognition Science. It realizes the T5 J-uniqueness step by setting J(x) to the average of x and its reciprocal minus one. Researchers on the forcing chain or phi-ladder cite this as the algebraic root for all cost properties. The declaration is a direct noncomputable definition with no proof obligations.
claimThe J-cost function on positive reals is defined by $J(x) = (x + x^{-1})/2 - 1$.
background
The Jcost definition sits in the Cost.JcostCore module and introduces the core cost measure for Recognition Science. It matches the closed form given in the T5 landmark of the forcing chain, where J is the unique function satisfying the Recognition Composition Law. The expression is equivalent to cosh(log x) - 1 and serves as the starting point for symmetry, non-negativity, and quadratic bounds proved in sibling declarations.
proof idea
The declaration is a one-line definition that directly assigns the algebraic expression (x + x inverse)/2 minus 1 to Jcost(x).
why it matters in Recognition Science
This definition anchors the entire cost domain and feeds the suite of basic lemmas on J-cost. It fills the T5 slot in the UnifiedForcingChain by supplying the explicit J that satisfies the composition law, enabling later steps toward the phi-ladder, eight-tick octave, and D=3. No open questions attach at this foundational level.
scope and limits
- Does not restrict the domain to positive reals in the signature.
- Does not prove any properties of the function.
- Does not reference the composition law or phi.
- Does not connect to physical constants or units.
formal statement (Lean)
6noncomputable def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
proof body
Definition body.
7