fibonacci_square_conjecture_consistent
plain-language theorem explainer
The arithmetic identity F_12 = 144 = 12^2 holds with offset N = 142, so the Fibonacci-square selection for the galactic timescale rung is consistent. ILG and zero-parameter gravity authors cite this when closing the claim that ILG needs no free phenomenological scale. The proof is a pure witness: exhibit 142 and discharge the two equalities by native decision.
Claim. There exists a natural number $N$ such that $N = 142$, $N+2 = F_{12}$, and $F_{12} = 12^2$, where $F_n$ denotes the $n$th Fibonacci number.
background
Module G-004 formalizes the RS stance that gravity is emergent ledger curvature, not a spin-2 force. Three concrete claims sit here: the coupling $\kappa = 8\varphi^5$ is algebraic in $\varphi$ alone (no gauge generator), GW polarizations equal 2 in $D=3$, and the BMV entanglement rate is a sharp RS number.
The Fibonacci-square selection is the arithmetic hinge that pins the galactic timescale rung. The proposition asserts existence of $N$ with $N=142$, $N+2=F_{12}$, and $F_{12}=12^2$. Sibling material (kappa_from_phi_alone, kappa_fibonacci_form) treats $\kappa$ as number-theoretic in $\varphi$; this identity is the discrete check that the rung choice is not an extra free parameter.
Upstream, the proposition is only a Prop package. The present theorem discharges it by computation, converting the named "conjecture" into a proved fact inside the same module.
proof idea
Term-mode existential introduction. The witness is the triple $(N,\mathrm{eq}_1,\mathrm{eq}2,\mathrm{eq}3)$ with $N:=142$. Reflexivity gives $N=142$. The remaining two Nat equalities $142+2=F{12}$ and $F{12}=12^2$ are closed by native_decide (both sides evaluate to 144). No lemmas beyond the definition of the proposition and Mathlib Fibonacci are required.
why it matters
Inside the NoGraviton registry item, this closes the arithmetic side of the zero-parameter ILG claim: if the Fibonacci-square identity holds, ILG carries no free galactic timescale rung; if it failed, that rung would remain one phenomenological parameter. The module header states the dichotomy explicitly.
The result sits beside kappa_from_phi_alone and kappa_fibonacci_form, reinforcing that gravitational strength in RS is forced by $\varphi$ and discrete ladder arithmetic (T6 fixed point, mass/rung ladder) rather than a gauge coupling. It does not itself prove absence of a graviton; it removes one potential free constant that would otherwise weaken the emergent-only story (G-004 claims 1–3).
No downstream consumers are wired yet (used_by empty), so the theorem is presently a self-contained consistency seal for the rung choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.