Jcost
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.