fibonacci_square_conjecture
plain-language theorem explainer
Names the Fibonacci-square selection as an explicit proposition: some natural N equals 142, N+2 equals the twelfth Fibonacci number, and that number equals 12 squared. ILG and emergent-gravity authors cite it when counting free parameters on the galactic timescale rung. The declaration is a Prop packaging only; a sibling theorem discharges it by native decision on the witness 142.
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 standard Fibonacci sequence ($F_0=0$, $F_1=1$).
background
Module G-004 formalizes the Recognition Science resolution that gravity is emergent curvature of the ledger lattice, not a force mediated by a spin-2 particle. Concrete claims in the module include: the coupling $\kappa$ is algebraic in $\varphi$ alone (no gauge generator), gravitational-wave polarizations equal 2 in $D=3$, and a BMV entanglement-rate prediction.
Fibonacci data enter from two nearby definitions: a Gap45 variant with $F(0)=F(1)=1$, and the standard/Mathlib sequence with $F(0)=0$, $F(1)=1$. The proposition uses the latter (Nat.fib), for which $F_{12}=144=12^{2}$.
The named selection packages that numerical coincidence together with the offset $N=142$ as a rung marker used when counting phenomenological parameters in information-limited gravity (ILG).
proof idea
No proof body: this is a definition of a Prop. It expands to a single existential whose matrix is the conjunction $N=142$, $N+2=\mathrm{Nat.fib},12$, and $\mathrm{Nat.fib},12=12^{2}$. Consistency is not argued here; the sibling theorem supplies the witness $\langle 142,\mathsf{rfl},\ldots\rangle$ and closes the two Fibonacci equalities by native_decide.
why it matters
Direct parent is the consistency theorem in the same module, whose doc-comment states the parameter-count fork: if the selection holds, ILG has zero phenomenological parameters; if not, one free parameter remains (the galactic timescale rung).
That fork sits beside the module's other G-004 claims: $\kappa$ forced from $\varphi$ alone (no graviton gauge coupling), two GW polarizations from $D=3$, and the BMV rate $\kappa_{\mathrm{rs}}\approx 88.7$. Fibonacci structure is the number-theoretic shadow of the phi-ladder and the forcing chain (T6 self-similar fixed point, eight-tick octave), so naming this selection ties the rung arithmetic to the claim that gravity needs no independent mediator quantum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.