ledgerCompose
plain-language theorem explainer
ledgerCompose defines additive composition of scales in the Recognition Science ledger as their arithmetic sum. Researchers deriving the golden ratio from closure axioms cite it when substituting into the scale sequence to obtain r² = r + 1. The definition is a direct abbreviation realizing the additive ledger axiom from the module's three-axiom setup.
Claim. The composition of two scales with values $a$ and $b$ is defined to be their sum $a + b$.
background
The Phi Forcing Derived module starts from three axioms: a discrete geometric scale sequence, additive ledger composition of recognition events, and closure of the sequence under that composition. Additive composition follows because the J-cost $J(x) = ½(x + 1/x) - 1$ is additive for independent events, so total recognition work tracked by the ledger is a sum rather than a product. The upstream Composition class from CostAxioms supplies the d'Alembert equation $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ that enforces multiplicative consistency, yet the ledger itself records additive totals.
proof idea
Direct definition that sets ledgerCompose a b to a + b. Downstream proofs such as closure_forces_golden_equation unfold the abbreviation to replace the composition symbol with ordinary addition inside the closure predicate.
why it matters
The definition supplies the concrete operation required by the hierarchy emergence theorems. It is invoked in hierarchy_emergence_forces_phi and ledger_forces_phi to conclude that the scale ratio equals phi, and in closure_forces_golden_equation to derive r² = r + 1. It therefore occupies the additive-composition slot in the T5-to-T6 bridge that forces the self-similar fixed point from ledger primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.