ledgerCompose
ledgerCompose defines the additive composition of two scales as their numerical sum. Researchers deriving the golden ratio from closure axioms cite it when unfolding the condition that a composed scale must remain in the geometric sequence. The definition is a direct abbreviation of real addition.
claimFor scales $a, b > 0$, the composition operation is defined by $a + b$.
background
The module derives $r^2 = r + 1$ from three axioms: scales form a geometric sequence, composition of recognition events is additive in the ledger (tracking total work), and the result must stay inside the sequence. The J-cost $J(x) = 1/2(x + 1/x) - 1$ supplies the additivity, since independent events accumulate J-cost by summation. This definition realizes the second axiom inside the GeometricScaleSequence structure.
proof idea
One-line definition that directly returns the sum of the two real arguments. Downstream lemmas such as closure_forces_golden_equation unfold ledgerCompose to replace the composition symbol with ordinary addition before invoking the geometric-sequence indexing.
why it matters in Recognition Science
It supplies the concrete additive operation required by the closure axiom, enabling the step from UniformScaleLadder to the conclusion that the ratio equals phi in hierarchy_emergence_forces_phi and ledger_forces_phi. The definition therefore sits at the T5-to-T6 bridge, converting the Recognition Composition Law into the self-similar fixed-point equation $r^2 = r + 1$.
scope and limits
- Does not restrict the domain of scales beyond the reals.
- Does not prove commutativity or associativity (those appear in separate lemmas).
- Does not encode the J-cost function or the d'Alembert equation.
- Does not address higher-dimensional or non-uniform ladders.
formal statement (Lean)
85def ledgerCompose (a b : ℝ) : ℝ := a + b
proof body
Definition body.
86
87/-- Composition is commutative -/