thirteen_is_fib_7
The natural number 13 equals the seventh Fibonacci number. Researchers building the Recognition Science cardinality spectrum cite this to place 13 inside the phi-ladder decomposition of canonical domain sizes. The proof is a direct numerical verification performed by the decide tactic.
claim$13 = F_7$, where $F_n$ is the $n$th Fibonacci number.
background
The module collects witnesses that cardinalities of RS domain types belong to a structured spectrum reachable from the generators 2, 3, configDim 5 and gap45. Fibonacci numbers enter because the phi-ladder (from PhiForcingDerived) produces self-similar sequences whose terms satisfy the same recurrence. Upstream, SpectralEmergence.of supplies the structural origin of the small integers 3 and 8 that seed the spectrum, while ArithmeticOf.canonical supplies the underlying Peano arithmetic used to compute the equality.
proof idea
One-line wrapper that applies the decide tactic to confirm the equality.
why it matters in Recognition Science
The declaration supplies an explicit member of the C21 spectrum, confirming that 13 decomposes cleanly via the phi-ladder. It supports the broader claim that RS cardinalities are not arbitrary but arise from the same forcing chain that yields D = 3 and the eight-tick octave. No downstream use sites are recorded yet.
scope and limits
- Does not prove that 13 appears as a physical cardinality in any concrete RS domain.
- Does not derive the Fibonacci recurrence from the Recognition Composition Law.
- Does not connect the equality to mass formulas or coupling constants.
- Does not address whether larger Fibonacci numbers remain inside the spectrum.
formal statement (Lean)
103theorem thirteen_is_fib_7 : (13 : ℕ) = Nat.fib 7 := by decide
proof body
Term-mode proof.
104
105/-! ## The spectrum: list of first 20 canonical RS cardinalities. -/
106