jBit_pos
plain-language theorem explainer
The theorem establishes that the link-penalty cost, defined as the natural logarithm of the golden ratio phi, is strictly positive. Researchers working on topological vetoes and finite-energy constraints in the Recognition framework cite this to bound the number of link crossings under any finite budget. The proof unfolds the definition of phi and applies the inequality 1 < sqrt(5) followed by linarith.
Claim. $0 < J_{bit}$ where $J_{bit} = ln phi$ and $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
In the log-domain J-cost geometry of Foundation paper F1, the canonical reciprocal cost is J(x) = ½(x + x^{-1}) - 1. The quantity jBit is introduced as the minimal nonzero ledger bit cost, given explicitly by the natural logarithm of phi. This module extends core identities from JcostCore to support geometric-mean optimality and simultaneous versus sequential descent.
proof idea
The proof unfolds the definition of phi. It establishes 1 < sqrt(5) by rewriting 1 as sqrt(1) and applying Real.sqrt_lt_sqrt to the pair (1,5). Linarith then combines the resulting inequalities to conclude that the logarithm is positive.
why it matters
This result supplies the positivity of the per-crossing cost required by finite_capacity_veto, which shows rigid rotation cannot arise from finite-energy initial data because infinitely many link crossings would exceed any finite budget. It also directly supports link_penalty_positive. Within the framework it anchors the phi-ladder scaling and the eight-tick octave in T5-T7 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.