qJ_pos
plain-language theorem explainer
Any positive rational ratio other than 1 has strictly positive rational J-cost. Cosmogenesis and ledger-cost arguments cite this to guarantee that a genuine distinction posts a nonzero cost. The proof rewrites J as a squared-defect over twice the ratio and checks both factors are positive.
Claim. For every rational $x>0$ with $x\neq 1$, the recognition cost $J(x)=(x+x^{-1})/2-1$ satisfies $J(x)>0$.
background
This module is the computable rational mirror of the real cosmogenesis dynamics in PreBigBang and FirstTick. Events carry rational ratios; double-entry posting adds each event with its reciprocal; total ledger cost is the sum of J-costs.
The cost used here is the canonical recognition cost over $\mathbb{Q}$:
$J(x)=(x+x^{-1})/2-1$.
It is the same algebraic form forced at T5 in the unified forcing chain (equivalently $\cosh(\log x)-1$), specialized to rationals so the simulation is #eval-able and kernel-checked.
Positivity of $J$ away from the identity is the elementary fact that a posted ratio distinct from unity is a genuine distinction and therefore incurs cost. The module later uses the self-similar recurrence $r\mapsto 1+1/r$ (Fibonacci convergents to $\varphi$) as seed ratios for the eight-tick run.
proof idea
Algebraic identity first: unfold $J$ and clear denominators to obtain $J(x)=(x-1)^2/(2x)$ (field simplification plus ring). Because $x\neq 1$, the factor $x-1$ is nonzero, so its square is strictly positive. The denominator $2x$ is positive from $x>0$. A positive-over-positive quotient is positive.
why it matters
Feeds seed2_first_tick_cost_pos, which asserts that the canonical seed-2 cosmogenesis run posts a genuine distinction at tick 0: the first-tick cost is positive. That certificate is part of the kernel-checked rational cosmogenesis package (flow-product conservation, eight-tick octave, emergence of $\varphi$ as exact Fibonacci convergents).
In the broader framework this is the rational shadow of T5 J-uniqueness and the Recognition Composition Law cost: identity has zero cost, every other positive ratio has positive cost. Without it, the simulation could not certify that the opening ledger post is a real distinction rather than a free no-op.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.