recurSeq_pos
plain-language theorem explainer
A positive rational seed stays strictly positive under the self-similar map r ↦ 1 + 1/r at every natural step. Cosmology and ledger proofs cite it to guarantee inverses and J-costs are well-defined on the rational Fibonacci convergents to φ. The argument is induction on the step index, using positivity of reciprocals and a one-line linear arithmetic close.
Claim. If $s \in \mathbb{Q}$ satisfies $s > 0$, then for every $t \in \mathbb{N}$ the iterate defined by $r_0 = s$ and $r_{t+1} = 1 + r_t^{-1}$ obeys $r_t > 0$.
background
This module is the computable, kernel-checked mirror of cosmogenesis: the same dynamics proved over $\mathbb{R}$ in PreBigBang and FirstTick are realized over $\mathbb{Q}$ so the run is a Lean object one can #eval, with conservation proved in the kernel.
The self-similar recognition recurrence $r \mapsto 1 + 1/r$ is defined as recurSeq: seed at step 0, then one plus the reciprocal. Its values are the exact Fibonacci convergents $2, 3/2, 5/3, 8/5, 13/8, \ldots$, which converge to $\varphi$. The recognition ledger over $\mathbb{Q}$ posts events with ratios drawn from this sequence; J-cost and flow-product identities need those ratios nonzero and positive.
Positivity of the seed is the only hypothesis. Reciprocals of positive rationals remain positive, so the inductive step stays inside $\mathbb{Q}_{>0}$.
proof idea
Induction on the discrete time index $t$.
Base case $t = 0$: the claim is exactly the seed hypothesis $0 < s$.
Successor: the inductive hypothesis gives $0 < r_n$. Mathlib inv_pos yields $0 < r_n^{-1}$. The goal $0 < 1 + r_n^{-1}$ is then closed by linarith. No external RS lemmas are required beyond the recursive definition of the sequence.
why it matters
Without strict positivity the rational cosmogenesis cannot invert ratios or form J-costs. Downstream, cosmogenesis_conserves feeds (recurSeq_pos seed hs t).ne' into the fold that proves the flow product equals $1$ at every agent after the full 8-tick run, for any positive seed (σ conservation, no decide, no sorry). Separately, seed2_first_tick_cost_pos uses the $t=0$ instance at seed $2$ to obtain a positive first-tick J-cost via qJ_pos.
In the broader framework this sequence is the exact rational witness that $\varphi$ emerges from the self-similar fixed-point dynamics (T6), visible tick-by-tick inside the eight-tick octave (T7) cosmogenesis simulation. It is a small arithmetic lemma, but it is the gate that keeps the entire $\mathbb{Q}$ ledger well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.