Jcost
The J-cost function is defined by J(x) = (x + 1/x)/2 - 1 for x > 0. Researchers deriving gravitational structure from the Recognition Composition Law cite this explicit form as the unique cost functional forced at T5. The implementation is a direct one-line definition with no lemmas or tactics applied.
claim$J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
Recognition Science obtains all physics from one functional equation. The Recognition Composition Law requires J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The supplied definition gives the explicit solution that satisfies this identity and the uniqueness condition stated in the module doc-comment. The local setting is the energy-processing bridge that links coherence fall to gravitational modifiers.
proof idea
Direct definition. The body is the algebraic expression already stated in the doc-comment; no lemmas are invoked and no tactics are used.
why it matters in Recognition Science
This supplies the J-cost that appears in T5 of the unified forcing chain and feeds every subsequent energy-distribution result in the gravity module. It anchors the transition from the Recognition Composition Law to the phi-ladder and the eight-tick octave. No open scaffolding is closed here; the definition simply makes the T5 object available for downstream use.
scope and limits
- Does not prove non-negativity of J(x).
- Does not derive uniqueness from the Recognition Composition Law.
- Does not embed the domain restriction x > 0 into the Lean type.
- Does not reference phi, the eight-tick octave, or the alpha band.
formal statement (Lean)
33def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
proof body
Definition body.
34