seed2_distinction
plain-language theorem explainer
The seed-2 recognition recurrence opens at ratio 2, not the identity ratio 1, so tick 0 posts a genuine distinction. First-tick cost and cosmogenesis certificates cite this to unlock a strictly positive J-cost at the opening event. The proof is a one-line native decision on the rational seed value.
Claim. Let $r_0=2$ and $r_{n+1}=1+1/r_n$ be the self-similar recognition recurrence over $\mathbb{Q}$. Then $r_0 \neq 1$.
background
The cosmogenesis simulation module mirrors the real-valued PreBigBang and FirstTick dynamics over $\mathbb{Q}$, so the ledger is a Lean object one can evaluate and check in-kernel. Events carry rational ratios; double-entry posting adds each event with its reciprocal; the per-tick cost increment is $+2J(r)$ with $J$ the standard recognition cost.
The self-similar recurrence $r \mapsto 1+1/r$ is defined over $\mathbb{Q}$ and yields the exact Fibonacci convergents $2, 3/2, 5/3, 8/5, \ldots$ to $\varphi$. By definition its value at step $0$ is the seed itself. A posted ratio equal to $1$ is not a distinction: $J(1)=0$, so positivity of first-tick cost needs the opening ratio off $1$.
The fundamental time quantum is one tick ($\tau_0=1$); the full cosmogenesis window is the eight-tick octave.
proof idea
Unfolding the recurrence at step $0$ gives the seed: the left-hand side is definitionally $2$ in $\mathbb{Q}$. The goal is therefore $2 \neq 1$, which native_decide discharges by kernel computation on rationals. No lemmas about positivity or later iterates are required.
why it matters
Downstream, seed2_first_tick_cost_pos applies the positivity lemma for $qJ$ to the seed-2 opening ratio and needs this inequality as the non-degeneracy hypothesis: without $r_0 \neq 1$ the first-tick cost could vanish. That certificate is the computable counterpart of the real FirstTick ledger increment and anchors the default seed-2 cosmogenesis run used by the golden-trace microkernel checks.
In the broader framework the same recurrence is the rational witness that $\varphi$ emerges as the self-similar fixed point (forcing chain T6), inside the eight-tick octave (T7). The result is small but load-bearing: it is the exact rational gate that turns the seed-2 simulation into a strictly costly opening distinction rather than a null post.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.