finite_capacity_veto
plain-language theorem explainer
The finite capacity veto establishes that no nonnegative real budget can bound every natural multiple of the positive link-penalty cost ln φ. Researchers examining blow-up limits for finite-energy data in three-dimensional topology cite it to exclude rigid rotation. The proof proceeds by contradiction: positivity of ln φ produces an explicit natural number N such that N times ln φ exceeds the budget, after which linear arithmetic finishes the argument.
Claim. Let $b$ be a real number with $b$ nonnegative. Then it is not the case that $N$ times ln φ is at most $b$ for every natural number $N$.
background
Module F6 treats topological capacity veto in three dimensions, with linking invariants, link penalties, and finite-budget obstructions as central objects. The constant jBit is defined in JCostGeometry as Real.log phi and satisfies jBit_pos, which asserts strict positivity. Cost functions imported from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost of recognition events and comparators on positive ratios. The local setting is the abstract budget obstruction that prevents infinite link crossings from finite initial data.
proof idea
The tactic proof assumes the contrary statement that every natural multiple of jBit stays below the budget. It obtains jBit_pos for strict positivity, then constructs N explicitly as Nat.floor(budget / jBit) plus one. Nat.lt_floor_add_one together with field_simp and mul_lt_mul_of_pos_right yields budget less than N times jBit. The assumption evaluated at this N and linarith produce the contradiction.
why it matters
The declaration is listed among the five main results of the F6 module on topological capacity veto in D equals 3. It supplies the abstract budget obstruction that supports the master veto: finite helicity implies finitely many crossings, each costing positive ln φ, so rigid rotation with zero linking cannot arise from finite-energy data. In the Recognition framework it enforces the finite-budget constraint consistent with the phi-ladder costs and the requirement of D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.