J_cost_motivates_additive_composition
plain-language theorem explainer
The theorem shows that when J-costs of two positive scales satisfy J(a) J(b) = 0, the composition identity collapses to J(ab) + J(a/b) = 2(J(a) + J(b)). Researchers deriving the golden ratio from ledger closure axioms cite it to justify why scale composition must be additive. The proof is a direct one-line application of the independent-events lemma.
Claim. For positive reals $a, b$ with $J(a) J(b) = 0$, where $J(x) = ½(x + x^{-1}) - 1$, the identity $J(ab) + J(a/b) = 2(J(a) + J(b))$ holds.
background
J-cost is the function $J(x) := ½(x + 1/x) - 1$ that quantifies recognition cost of a scale ratio. The module derives $r^2 = r + 1$ from three axioms: geometric scale sequences, additive ledger composition of events, and closure of the sequence under that composition. This theorem supplies the physical motivation for the additive axiom by linking it to the vanishing-interaction regime of J-cost. It rests on the upstream lemma that the full RCL identity reduces to additivity precisely when the cross term $J(a) J(b)$ is zero.
proof idea
The proof is a one-line wrapper that applies J_additive_for_independent, passing the positivity hypotheses and the independence assumption directly to that lemma.
why it matters
The result grounds the additive ledger axiom used in the complete phi forcing theorem of the same module, which concludes that the unique positive closed ratio is phi. It forms part of the T5 to T6 bridge in the forcing chain, where J-uniqueness motivates the self-similar fixed point. The module comment explicitly ties this additivity to the physical requirement that total recognition work be additive for independent events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.