link_penalty_positive
plain-language theorem explainer
The theorem establishes that the per-crossing topological penalty equals ln phi and is strictly positive. Researchers bounding helicity in three-dimensional finite-energy fields cite it to enforce the capacity veto. The proof is a direct term application of the positivity result for the logarithm of the golden ratio.
Claim. The link-penalty cost per topological crossing satisfies $0 < J_{bit}$ where $J_{bit} = ln phi$ and phi denotes the golden ratio.
background
The module develops the topological capacity veto for three-dimensional space under the Recognition framework. It establishes that integer linking invariants exist only in D=3 and that each crossing of linked loops carries a positive cost drawn from the J-cost geometry. The local setting is the finite-helicity budget that follows from the eight-tick periodicity (F6=8).
proof idea
One-line wrapper that applies the upstream theorem jBit_pos. That theorem unfolds the definition jBit = Real.log phi and invokes Real.log_pos together with the inequality 1 < phi derived from the square-root properties of the golden ratio.
why it matters
It supplies the strict positivity required for the finite-capacity veto (F6.2.3) and the finite-crossings implication in the same module. The result closes the step from J-cost geometry to bounded topological complexity under finite energy in D=3. It fills the F6.2.1 slot in the foundation paper and connects directly to the eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.