J
plain-language theorem explainer
J assigns to each positive real scale ratio its J-cost, the additive quantity measuring recognition work. Researchers deriving the golden ratio from ledger closure axioms cite this when decomposing total costs across independent events. The definition is a direct one-line alias to the Jcost implementation, which encodes the closed-form expression satisfying the recognition composition law.
Claim. Let $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$, the J-cost of a scale ratio $x$ that is additive under independent recognition events.
background
The module derives $r^2 = r + 1$ from three axioms: discrete geometric scale sequences, additive ledger composition for total recognition work, and closure under composition. The J-cost supplies the key insight that total cost of independent events equals the sum of individual costs, forcing the scale ratio to satisfy the quadratic. Upstream results include the cost induced by multiplicative recognizers, the J-cost of observer forcing events (non-negative, zero at the identity event of scale 1), and structures for nuclear densities on phi-tiers.
proof idea
This definition is a one-line wrapper that directly invokes the Jcost implementation from the Cost module.
why it matters
This supplies the explicit J function realizing T5 J-uniqueness in the forcing chain, enabling the recognition composition law and the derivation of phi as the self-similar fixed point. It supports the phi-ladder mass formulas and the eight-tick octave structure. The module bridges the stated closure axiom to the concrete scale ratio phi, feeding siblings such as phi_forcing_complete and J_composition_decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.