recurSeq
plain-language theorem explainer
The self-similar map r ↦ 1 + 1/r iterated over the rationals from a seed, yielding the exact Fibonacci convergents 2, 3/2, 5/3, 8/5, … to φ. Cosmogenesis and ledger-cost arguments cite it as the tick-by-tick ratio sequence on the 3-cube cadence. Defined by primitive recursion on ℕ; no proof content.
Claim. For a rational seed $s$, define the sequence $(r_n)_{n\in\mathbb{N}}$ by $r_0 = s$ and $r_{n+1} = 1 + r_n^{-1}$. The terms are the exact Fibonacci convergents to $\varphi$ when $s=2$.
background
The module CosmogenesisSim is a computable mirror, over $\mathbb{Q}$, of the real-valued PreBigBang and FirstTick dynamics. Recognition events, reciprocal double-entry, and J-cost are all rational so the full eight-tick run can be #eval'd and conservation proved in-kernel.
The recurrence $r \mapsto 1 + 1/r$ is the discrete self-similarity whose unique positive fixed point is $\varphi$ (forcing chain T6). Starting from a positive rational seed it produces the Fibonacci ratios exactly: $2, 3/2, 5/3, 8/5, 13/8, \ldots$, which converge to $\varphi$ in $\mathbb{R}$ but remain exact rationals at every finite tick.
Sibling defs (QEvent, qJ, qcost, addEvent) post these ratios as ledger edges on the 3-cube cadence; the flow product is the multiplicative conserved quantity.
proof idea
Pure recursive definition on $\mathbb{N}$: base case returns the seed; successor applies $r \mapsto 1 + r^{-1}$. No tactics, no lemmas. Downstream positivity (recurSeq_pos) is proved separately by induction using inv_pos.
why it matters
Supplies the tick-indexed ratio that cosmoEvent loads onto each edge of the eight-tick 3-cube cadence, and that seed2_distinction / seed2_first_tick_cost_pos use to certify a genuine nonzero first-tick J-cost for the canonical seed-2 run. Those facts feed TraceCertificates and the kernel-checked trace_certificates_seed2.
In the Recognition framework this is the discrete witness that φ emerges as the self-similar fixed point (T6) already at the rational level, before any real completion. The module doc states the sequence makes "the emergence of φ visible as an exact rational sequence." It does not itself force φ; it exhibits the orbit whose limit is φ and whose finite values drive the cosmogenesis ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.