Foundation Topological Veto Finite Crossings From Budget

The budget bound

In the Recognition Science framework, the declaration finite_crossings_from_budget establishes a plain arithmetic fact about budgets and costs. It states that if you have a nonnegative budget, and each operation (here, a topological crossing of linked loops) has a positive cost, then the number of operations you can afford is bounded by the budget divided by the cost. The theorem is a formal restatement of an everyday constraint: with a finite pile of money and a positive price per item, you can buy only finitely many items.

The declaration is a general lemma about real numbers, proved in the framework's machine-checked library of formal theorems. It takes as premises a nonnegative budget, a positive cost per crossing, and a number n whose total cost fits within the budget. Its conclusion is that n is at most budget divided by cost. The proof is a direct application of a more general finite-operations lemma; no physics enters the arithmetic. This is the kind of result that makes the framework's later claims about three-dimensional space and linking precise: it guarantees that finite energy cannot fund an infinite cascade of topological changes.

What the declaration does not claim is equally important. It does not assert that any particular physical system has a finite budget, nor that crossings are the only cost in the framework. It does not say what the cost per crossing actually is; that value, the framework's minimal nonzero ledger bit cost ln φ, is supplied by a separate theorem. The declaration is a conditional statement: if the budget is finite and the cost is positive, then the number of crossings is finite. It is a tool for other arguments, not a claim about the world on its own.

The consequence is a clean veto on infinite complexity. The framework uses this bound to argue that rigid rotation, which would require zero linking over infinite extent, cannot arise from finite-energy initial data, because transitioning to it would require infinitely many crossings at positive cost. That larger argument depends on additional premises about helicity and linking; the budget bound itself only establishes the arithmetic ceiling.

/-- **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

/-- **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

/-- **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

What this page does not claim

The declaration does not claim that any actual physical system has a finite budget. It does not claim that crossings are the only cost in the framework. It does not establish the specific value of the cost per crossing.

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: