ledgerCompose_assoc
plain-language theorem explainer
The lemma states that ledger composition on real numbers is associative. Workers on geometric scale sequences in Recognition Science cite it to confirm that iterated additive compositions of scales remain well-defined inside the sequence. The proof is a one-line wrapper that unfolds the definition of ledgerCompose to ordinary addition and invokes the ring tactic.
Claim. For all real numbers $a,b,c$, if ledger composition is defined by $a + b$, then $(a + b) + c = a + (b + c)$.
background
The module derives the golden-ratio equation from three axioms on scale sequences: scales form a geometric progression, composition of recognition events is additive on their scales (because the ledger records total recognition work), and the result of any composition must again lie in the sequence. ledgerCompose is the concrete operation realizing the second axiom: ledgerCompose(a,b) := a + b. The upstream Composition class from CostAxioms supplies the Recognition Composition Law that forces J-cost to be additive, providing the justification for using + rather than multiplication on the scales themselves.
proof idea
One-line wrapper that unfolds ledgerCompose to addition and applies the ring tactic.
why it matters
Associativity is required for the closure axiom (GeometricScaleSequence.isClosed) to be unambiguous when more than two scales are composed; without it the derivation that 1 + r = r² would not extend consistently to longer chains. The lemma therefore sits inside the T5-to-T6 bridge that forces the self-similar fixed point phi. It is a prerequisite for any later statement that multiple recognition events can be grouped without changing the total scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.