J_additive_for_independent
plain-language theorem explainer
When the product of J-costs vanishes, the composition identity for scales reduces to pure additivity: J(ab) + J(a/b) equals twice the sum of the separate costs. Researchers deriving the golden ratio from ledger closure axioms cite this to justify the additive scale rule from J-cost structure. The proof is a one-line wrapper that applies the general decomposition lemma and simplifies via linear arithmetic under the independence hypothesis.
Claim. Let $J(x) := ½(x + x^{-1}) - 1$. For $a, b > 0$ satisfying $J(a) · J(b) = 0$, the identity $J(ab) + J(a/b) = 2(J(a) + J(b))$ holds.
background
J is the J-cost function J(x) = Cost.Jcost x, satisfying the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y) via the sibling J_composition_decomposition. The module derives r² = r + 1 from three axioms: discrete geometric scales, additive ledger composition of scales (motivated by J-cost additivity), and closure under composition. MODULE_DOC states that J-total = J(a) + J(b) for independent events supplies the physical reason scales must add rather than multiply, linking to the T5→T6 bridge where closure forces phi.
proof idea
The term proof calls J_composition_decomposition a b ha hb to obtain the full identity containing the quadratic term 2 J(a) J(b), then applies nlinarith with the hypothesis J(a) J(b) = 0 to cancel that term and recover the additive form.
why it matters
This declaration feeds the downstream theorem J_cost_motivates_additive_composition, which supplies the explicit motivation for Axiom 2 (additive ledger composition) in the phi-forcing derivation. It connects the J-cost structure (T5 J-uniqueness) to the additive rule required for closure, which yields r = phi and the eight-tick octave. The result closes one link in the chain from J-cost to the D = 3 spatial dimensions and alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.