perEpochReach_pos
plain-language theorem explainer
For every epoch index k, the comoving distance covered by a recognition signal in that epoch is strictly positive. Cosmology proofs that need monotonic climb of cumulative reach, or a strictly positive tail in the geometric series to the 8φ² horizon, cite this. The argument unfolds the definition and multiplies the positivity of 8 by the positivity of (1/φ)^k.
Claim. For every natural number $k$, the per-epoch comoving reach is strictly positive: $0 < 8\,(1/\varphi)^k$, where $\varphi$ is the golden ratio.
background
This module builds the finite recognition event horizon that drives Phase-9 freeze-out. A recognition signal advances one comoving cell per tick; the eight-tick octave (T-7) therefore covers eight cells per epoch at unit scale. Self-similar dilation expands the comoving scale by $\varphi$ each epoch (T-6), so the distance covered in epoch $m$ is scaled by $\varphi^{-m}$.
Concretely, the per-epoch reach is defined as $8,(1/\varphi)^m$. The ratio $1/\varphi$ is positive because $\varphi>0$. The cumulative reach is the partial sum of these terms; the infinite sum converges to the de Sitter recognition horizon $8\varphi^2\approx 20.944$ comoving cells, using $\varphi^2=\varphi+1$.
Positivity of each summand is the elementary gate before monotonicity and strict sub-horizon bounds.
proof idea
Term-mode after unfold: rewrite the goal as $0<8\cdot(1/\varphi)^k$. Apply the real product-positivity rule to the pair of factors. The first factor is discharged by norm_num ($8>0$). The second uses pow_pos on the local lemma that $0<1/\varphi$, itself from $\varphi>0$. No induction and no series machinery.
why it matters
Without a strictly positive increment each epoch, the cumulative reach would not be strictly monotone and the geometric tail would not be forced positive. Downstream, cumulativeReach_strictMono applies this at each $n$ via linarith after writing the successor sum as prior sum plus the $n$-th term. The companion theorem cumulativeReach_lt_horizon needs the same positivity culture when splitting the summable series and controlling the tail below $8\varphi^2$.
Framework-wise this is pure T-6/T-7 bookkeeping: cadence 8 and dilation $\varphi$, no fitted Hubble rate. It underwrites the physical claim that super-horizon structure never enters causal contact and freezes at primordial amplitude (the RS $\Omega_\Lambda$ freeze-out), while sub-horizon structure is eventually crossed and homogenized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.