discrete_fibonacci_from_minimality
plain-language theorem explainer
Natural-number coefficients α, β in the additive recurrence ℓ₂ = α ℓ₁ + β ℓ₀ must satisfy α = β = 1 under the zero-parameter minimality condition max(α, β) = 1. Researchers closing the discrete coefficient step in the posting extensivity derivation from the Recognition Composition Law would cite it to justify the Fibonacci recurrence. The proof is a short term-mode argument that splits the conjunction and applies antisymmetry on the naturals to the supplied bounds.
Claim. Let $a, b$ be natural numbers with $a ≥ 1$, $b ≥ 1$, and max$(a, b) = 1$. Then $a = 1$ and $b = 1$.
background
The module derives additive scale composition from the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y), where J(x) = ½(x + x⁻¹) − 1. Posting potential Π(x) := J(x) + 1 satisfies the d'Alembert identity that yields multiplicative composition for events whose costs combine via the RCL. In the self-similar regime this forces additive scale composition ℓ_{k+2} = ℓ_{k+1} + ℓ_k for geometric sequences closed under the first composition step. The local setting is the integer-coefficient step that follows from discreteness in a countable carrier, as part of closing Proposition 4.3 of the phi paper without assuming linearity a priori.
proof idea
The term proof opens with constructor to split the target conjunction. Each conjunct is discharged by Nat.le_antisymm (from ArithmeticFromLogic) applied to the lower bound (ha or hb) and an upper bound obtained from the max condition via omega.
why it matters
This result supplies the discrete-coefficients step that completes the posting-extensivity bridge: RCL → posting d'Alembert → additive closure → golden equation → φ. It directly supports the end-to-end claim in the module doc-comment that a geometric scale sequence closed under additive posting with discrete minimal coefficients forces φ. The declaration touches the open question of justifying the linear recurrence without external linearity assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.