finite_crossings_from_budget
plain-language theorem explainer
Finite nonnegative budget and positive cost per crossing bound the number of crossings by their ratio. Field theorists working on vortex linking and topological defects in three dimensions cite the bound to enforce finite complexity under energy constraints. The argument is a direct one-line application of the operation-counting lemma from pinch algebra after reordering hypotheses.
Claim. If $0 ≤ B$, $0 < c$, and $n ∈ ℕ$ satisfies $n · c ≤ B$, then $n ≤ B/c$.
background
The module develops the topological capacity veto for D = 3, where Alexander duality supplies an integer linking invariant and each crossing carries a positive penalty. The local results include that linking exists only in three dimensions, that the penalty is ln φ > 0, and that finite energy implies finitely many crossings. This theorem adapts the general counting bound to the crossing setting.
proof idea
The proof is a one-line wrapper that applies finite_operations_from_budget after reordering the cost and budget hypotheses to match its signature.
why it matters
It supplies the finite-crossings half of F6.3.2/3.3 and feeds directly into the contrapositive infinite_crossings_need_infinite_budget. The step supports the claim that rigid rotation cannot arise from finite-energy data in D = 3 and aligns with the eight-tick periodicity F6 = 8. It closes a link between pinch-algebra counting and topological veto.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.