J
plain-language theorem explainer
J defines the fundamental cost on positive reals by the algebraic rule J(x) = (x + 1/x)/2 - 1. Researchers working on the Recognition Science forcing chain cite this expression as the canonical cost that satisfies T5 uniqueness. The definition is a direct algebraic formula with no proof steps or additional hypotheses.
Claim. Define the cost function by the rule $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
This definition supplies the J-cost that appears throughout the Recognition Science framework. The accompanying doc-comment states that the expression is the unique cost satisfying d'Alembert's formula together with normalization and calibration conditions from T5. The module imports LawOfExistence and places the definition inside the modal domain where possibility and transition properties are developed.
proof idea
The declaration is a one-line definition that directly encodes the T5 uniqueness formula for the J-cost.
why it matters
The definition anchors T5 in the UnifiedForcingChain and supplies the cost that enters the Recognition Composition Law. Sibling declarations such as J_nonneg and J_transition derive their statements directly from this expression. It also supplies the native-unit constants and the phi-ladder mass formula used in later forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.