Foundation Topological Veto

The finite-capacity veto

In topology, two closed loops can be linked like rings of a chain, and the linking number is an integer that counts how many times one loop winds around another. A classical result, Alexander duality, says that this integer-valued linking invariant exists only in three dimensions: for an embedded circle in a sphere, the first homology group of the complement is isomorphic to the integers if and only if the dimension is 3. This is a standard fact of algebraic topology, and it is the reason three-dimensional space is special for knotting and linking.

Recognition Science builds on this classical fact through a machine-checked library of formal theorems. The framework models physical structure as a ledger, a discrete record of recognition events, where each event carries a forced cost. The minimal nonzero cost per ledger bit is ln φ, the natural logarithm of the golden ratio, which is positive. The library proves that each topological crossing of linked loops incurs this positive cost, so linking complexity is not free: it must be paid for from a finite energy budget.

The central result, the finite-capacity veto, states that a finite budget cannot fund infinitely many operations at positive cost. The proof is a simple counting argument: if each crossing costs c > 0 and the budget is B, then the number of crossings n must satisfy n · c ≤ B, so n ≤ B/c. Therefore, infinitely many crossings would require an infinite budget. The library formalizes this as the theorem finite_capacity_veto, which asserts the negation of the statement that every finite N crossings fit within the budget.

The veto applies to rigid rotation. In rigid rotation, all vortex lines are parallel straight lines, so their pairwise linking is zero. The library proves this as rigid_rotation_zero_linking. The master veto argument, stated as a proof sketch in the foundation paper, combines these facts: finite-energy initial data has finite helicity, meaning finite linking complexity; rigid rotation requires zero linking over infinite extent; transitioning from one to the other would require infinitely many link crossings; each crossing costs ln φ > 0; so a finite budget cannot cover the infinite cost. The full statement requires Navier-Stokes-specific objects, so the formal library states the abstract budget obstruction, not the fluid-dynamical conclusion.

What this establishes in plain language is a capacity constraint: a system with finite energy cannot realize a state whose topological complexity is infinite. The framework's contribution is to tie that constraint to a specific positive cost per crossing, derived from the golden ratio, and to formalize the counting argument in a machine-checked way. The consequence is that rigid rotation, as an idealized infinite-extent state, is not reachable from finite-energy initial data.

/-- **F6.1.1/1.2**: Alexander duality implies integer-valued linking exists iff D = 3.
    Statement: for embedded circle K ⊂ S^D, H₁(S^D \ K) ≅ Z iff D = 3.

    We state this as an axiom matching the already-proved result in
    `Verification.Dimension`. The full Alexander duality proof is
    classical algebraic topology. -/
theorem linking_requires_D3 (D : ℕ) (h : D ≥ 2) :
    -- "Nontrivial integer linking of disjoint loops is possible"
    -- is equivalent to D = 3 (Alexander duality)
    (∃ (_ : D = 3), True) ∨ D ≠ 3 := by
  by_cases h3 : D = 3
  · exact Or.inl ⟨h3, trivial⟩
  · exact Or.inr h3

/- OPEN: nontrivial integer linking of embedded loops in S^D exists iff D = 3
   (Alexander duality). Former `linking_nontrivial_iff_D3` concluded `True`
   from a vacuous `∃ _, True` hypothesis and was deleted. The nearby
   `linking_requires_D3` is itself still only a tautological packaging of
   `D = 3 ∨ D ≠ 3`; the classical duality content remains unpaid. -/

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

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

What this page does not claim

The library does not prove the full fluid-dynamical master veto; it proves the abstract budget obstruction. The framework does not claim that rigid rotation is physically impossible, only that it is not reachable from finite-energy data. The linking invariant's existence is assumed as an axiom in this module, not proved from first principles.

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: