Foundation Topological Veto Link Penalty Positive

The cost of a crossing

In the Recognition Science framework, a ledger is a discrete record of events, and each event has a cost. The declaration link_penalty_positive establishes the simplest possible fact about one kind of event: a topological crossing, where two loops pass through each other, has a positive cost. The theorem states that the cost per crossing is greater than zero, and in this framework that cost is exactly the natural logarithm of the golden ratio, about 0.4812. This is not a free parameter; it is the minimal nonzero cost that the framework's cost function permits.

The positive cost is the engine behind a larger result in the framework's library, a machine-checked collection of formal theorems. Because each crossing costs a positive amount, a finite budget of energy can fund only a finite number of crossings. The theorem finite_crossings_from_budget makes this precise: if you have a budget and each operation costs a positive amount, the number of operations you can afford is bounded by the budget divided by the cost. This is a purely arithmetic fact, but it carries a physical consequence. The framework uses it to argue that a state like rigid rotation, which would require an infinite pattern of linked or unlinked vortex lines, cannot arise from finite-energy initial data. The finite-capacity veto, as the framework calls it, is the conclusion that a finite budget cannot fund infinitely many crossings.

The declaration does not claim that any particular physical system actually contains such crossings, nor does it prove that rigid rotation is impossible in the real world. It proves a conditional statement: if you accept the framework's cost model, then a finite budget forbids infinitely many crossings. The theorem itself is a statement about real numbers and inequalities, not about fluid dynamics. The step from the arithmetic to a physical veto depends on identifying the framework's abstract cost with a physical energy, and that identification is a modeling choice, not a proved theorem. The framework's own documentation notes that the full physical statement requires objects specific to its Navier-Stokes treatment, which are not part of this declaration.

What the declaration changes is the shape of the argument. It turns a topological question, how many times can loops link, into a budget question, how many crossings can you afford. Once the cost per crossing is positive, the arithmetic of finite budgets does the rest. The reader can now see why the framework treats linking as a scarce resource rather than a free topological invariant.

/-- **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.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.5 Master Veto**: Rigid rotation cannot arise as a blow-up limit
    from finite-energy initial data.

    Proof sketch:
    1. Initial data has finite helicity (finite linking complexity)
    2. Rigid rotation requires zero linking over infinite extent
    3. Transitioning requires infinitely many link crossings
    4. Each crossing costs ln φ > 0
    5. Finite budget < infinite required cost: contradiction

    The full statement requires NS-specific objects; here we state the
    abstract budget obstruction. -/
theorem finite_capacity_veto (budget : ℝ) (hbudget : 0 ≤ budget) :
    -- Cannot fund infinitely many operations at positive cost
    ¬(∀ N : ℕ, (N : ℝ) * jBit ≤ budget) := by
  intro h
  -- For N large enough, N * jBit > budget
  have hjb := jBit_pos
  -- Take N = ⌊budget / jBit⌋ + 1
  have : ∃ N : ℕ, budget < (N : ℝ) * jBit := by
    use (Nat.floor (budget / jBit) + 1)
    push_cast
    have hfloor := Nat.lt_floor_add_one (budget / jBit)
    calc budget = (budget / jBit) * jBit := by field_simp
      _ < (↑(Nat.floor (budget / jBit)) + 1) * jBit := by
        exact mul_lt_mul_of_pos_right hfloor hjb
  obtain ⟨N, hN⟩ := this
  have hle := h N
  linarith

What this page does not claim

It does not claim that any physical system actually contains such crossings. It does not prove that rigid rotation is impossible in the real world, only that a finite budget forbids infinitely many crossings under the framework's cost model. It does not establish the physical identification between the abstract cost and physical energy; that step is a modeling choice.

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: