posting_gives_unit_recurrence
plain-language theorem explainer
The theorem establishes that additive closure at the second level of a uniform scale ladder forces the recurrence coefficients to be the unit pair (1,1) in real arithmetic. Researchers deriving linear scale composition from the Recognition Composition Law cite this as the step that extracts integer coefficients from discreteness without assuming linearity upfront. The proof is a term-mode one-liner that rewrites via the one_mul identity and matches the supplied closure hypothesis.
Claim. Let $L$ be a uniform scale ladder with level sizes $l_k = L.levels(k)$. If $l_2 = l_1 + l_0$, then $l_2 = 1·l_1 + 1·l_0$.
background
UniformScaleLadder is the structure of positive level sizes $l_k$ obeying uniform scaling $l_{k+1} = r · l_k$ with $r > 1$. The module derives additive scale composition from the Recognition Composition Law without presupposing linearity, closing Proposition 4.3 of the phi paper. The local setting begins from the RCL $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and shifts to posting potential $Π(x) = J(x) + 1$ to obtain multiplicative composition that forces additivity under self-similar closure.
proof idea
The proof is a one-line term wrapper. It applies the one_mul theorem from ArithmeticFromLogic, which states succ zero * n = n, to replace the implicit multiplication by 1, then uses exact to discharge the given closure hypothesis.
why it matters
This step supplies the unit coefficients required for the integer recurrence in the Posting Extensivity chain. It feeds the derivation of additive scale composition that closes Proposition 4.3 and supports later results on phi-forcing and discrete Fibonacci sequences from minimality. The declaration sits inside the module that converts RCL-governed cost composition into the linear recurrence $l_{k+2} = l_{k+1} + l_k$ without external linearity assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.