J_composition_decomposition
plain-language theorem explainer
The declaration supplies the exact algebraic identity satisfied by the J-cost under multiplicative scale composition. Researchers deriving the golden ratio from ledger closure axioms cite it as the concrete realization of the recognition composition law for this cost function. The proof is a direct algebraic verification obtained by unfolding the cost definition, clearing denominators, and normalizing the resulting polynomial identity.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then for all positive real numbers $a, b > 0$, $J(ab) + J(a/b) = 2 J(a) J(b) + 2 J(a) + 2 J(b)$.
background
The J-cost is defined as the recognition work associated to a scale ratio, with explicit form $J(x) = 1/2 (x + 1/x) - 1$. This module derives the equation $r^2 = r + 1$ from three axioms: discrete geometric scale sequences, additive ledger composition (total recognition work adds), and closure under composition. The J-cost supplies the required additivity because the total cost of independent events is the sum of the separate costs. The module thereby answers why the closure condition forces the golden ratio once the additive structure is in place.
proof idea
The proof is a term-mode algebraic check. It unfolds J to the underlying cost definition, uses the positivity hypotheses to obtain that a and b are nonzero, applies field simplification to clear denominators, and finishes with the ring tactic to confirm the identity.
why it matters
This identity directly feeds the additive-regime theorem in the same module, which recovers pure additivity when the cross term vanishes. It instantiates the recognition composition law inside the phi-forcing derivation, connecting to the T5 uniqueness of J and the self-similar fixed-point condition that forces phi. The module as a whole thereby closes the step from the stated closure axiom to the golden equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.