thirteen_is_fib_7
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.