posting_gives_unit_recurrence
The theorem establishes that additive closure at the second level of a uniform scale ladder forces the recurrence coefficients to be exactly the unit pair (1,1). Researchers deriving integer coefficients for scale hierarchies from the Recognition Composition Law would cite this result to confirm minimality without assuming linearity upfront. The proof is a one-line term wrapper that rewrites the right-hand side via the one_mul identity and matches the closure hypothesis directly.
claimLet $L$ be a uniform scale ladder (a sequence of positive real level sizes with uniform ratio greater than 1). If the additive closure $L(2) = L(1) + L(0)$ holds, then the recurrence takes the form $L(2) = 1 · L(1) + 1 · L(0)$.
background
UniformScaleLadder is the structure consisting of a levels function from naturals to positive reals, a ratio greater than one, and the uniform scaling property that each successive level is the ratio times the previous. The module PostingExtensivity derives additive scale composition from the Recognition Composition Law (RCL) without presupposing linearity, closing Proposition 4.3 of the phi paper. The RCL states that J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) with J(x) = ½(x + x⁻¹) − 1; posting potential is the shifted form Π(x) = J(x) + 1 that becomes multiplicative under RCL composition. Upstream, one_mul supplies the arithmetic identity succ(zero) * n = n, which here rewrites multiplication by one as the identity on reals.
proof idea
The term proof first invokes simp only [one_mul] to replace the right-hand side (1 : ℝ) * L.levels 1 + (1 : ℝ) * L.levels 0 with L.levels 1 + L.levels 0 using the one_mul lemma from ArithmeticFromLogic. It then applies exact to discharge the goal against the supplied closure hypothesis.
why it matters in Recognition Science
This result supplies the unit coefficients required for the integer-coefficients step in the module's derivation of additive scale composition from RCL, directly supporting closure of Proposition 4.3. It sits inside the chain from forced RCL through posting potential and extensive posting to the self-similar fixed point phi and the eight-tick octave. The declaration confirms that discreteness plus closure forces the minimal (1,1) pair before higher-level or nonlinear extensions are considered.
scope and limits
- Does not prove the additive closure hypothesis; it assumes the equality as input.
- Does not extend the recurrence relation beyond level 2.
- Does not invoke the uniform scaling ratio or positivity constraints inside the statement.
- Does not rule out nonlinear recurrences compatible with geometric scaling.
formal statement (Lean)
188theorem posting_gives_unit_recurrence
189 (L : UniformScaleLadder)
190 (closure : L.levels 2 = L.levels 1 + L.levels 0) :
191 L.levels 2 = (1 : ℝ) * L.levels 1 + (1 : ℝ) * L.levels 0 := by
proof body
Term-mode proof.
192 simp only [one_mul]; exact closure
193
194/-- The unit pair (1, 1) is minimal: max(1, 1) = 1. -/