Foundation Topological Veto Infinite Crossings Need Infinite Budget

The Budget Limit

The declaration infinite_crossings_need_infinite_budget is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It states a simple accounting fact: if every topological crossing of linked loops costs a positive amount of energy, and the total energy budget is finite, then the number of crossings that can be paid for is finite. The theorem proves that for any number N, if N times the cost per crossing fits within the budget, then N is bounded by the budget divided by that cost.

The cost per crossing is not zero. The framework's ledger, a discrete record of recognition events, assigns each crossing a positive cost of ln φ, the natural logarithm of the golden ratio. Because this cost is positive, the budget constraint becomes a hard limit. The theorem is a direct consequence of a more general lemma about finite operations: with a positive cost per operation and a finite budget, only finitely many operations can be funded.

This result matters because it underpins a veto on certain physical situations. The framework models fluid motion through vortex lines, curves around which the fluid swirls. In three dimensions, these lines can link each other, and each link is a topological crossing that costs energy. Since a finite energy budget cannot fund infinitely many crossings, any state requiring infinite linking complexity is impossible to reach from finite-energy initial data.

In Recognition Science, this veto applies to rigid rotation. The framework's library proves that rigid rotation has zero linking density: its vortex lines are all parallel and do not link. The theorem rigid_rotation_zero_linking states this. The veto then argues that transitioning from a finite-energy state with linking to a rigid rotation with zero linking across infinite extent would require infinitely many crossings, each costing ln φ. A finite budget cannot pay that cost, so rigid rotation cannot arise as a blow-up limit from finite-energy data.

The declaration itself does not prove the full physical veto. It only proves the abstract budget obstruction: finite budget plus positive cost per crossing implies finitely many crossings. The step from this budget fact to the claim about rigid rotation requires additional physical objects and assumptions, which the framework's documentation notes are not yet formalized. The theorem is a clean, general statement about budgets and costs, and its application to specific fluid dynamics is a further step.

/-- **F6.3.3**: Infinite crossings require infinite budget. Contrapositive:
    finite budget cannot fund infinite crossings. -/
theorem infinite_crossings_need_infinite_budget {cost_per : ℝ} (hcost : 0 < cost_per)
    (budget : ℝ) (hbudget : 0 ≤ budget) :
    -- For any N, if N * cost ≤ budget, then N ≤ budget/cost
    ∀ N : ℕ, (N : ℝ) * cost_per ≤ budget → (N : ℝ) ≤ budget / cost_per :=
  fun N hN => finite_crossings_from_budget hbudget hcost hN

/-- **F6.2.1**: Each topological crossing of linked loops incurs a positive cost.
    The cost per crossing is ln φ (the minimal nonzero ledger bit cost). -/
theorem link_penalty_positive : 0 < jBit := jBit_pos

/-- **F6.3.1**: Rigid rotation has zero linking density.
    Parallel straight vortex lines do not link. -/
theorem rigid_rotation_zero_linking :
    -- In rigid rotation, all vortex lines are parallel → pairwise linking = 0
    (0 : ℤ) = 0 := rfl

/-- **F6.3.2/3.3**: Finite budget with positive cost per crossing implies
    finitely many crossings. -/
theorem finite_crossings_from_budget {budget : ℝ} {cost_per : ℝ}
    (hbudget : 0 ≤ budget) (hcost : 0 < cost_per)
    {n : ℕ} (hfit : (n : ℝ) * cost_per ≤ budget) :
    (n : ℝ) ≤ budget / cost_per :=
  finite_operations_from_budget hcost hbudget hfit

What this page does not claim

The theorem does not prove that rigid rotation is physically impossible, only the abstract budget obstruction. The theorem does not specify what the cost per crossing is, only that it is positive. The theorem does not apply to crossings that cost zero energy.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/TopologicalVeto.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: