Verification Dimension Linking

Dimension linking

Recognition Science (a framework that derives physical structure from a ledger, a discrete record of recognition events) treats space itself as a consequence of how objects link. The module Verification.DimensionLinking checks the topology behind this claim. Its central result is a theorem: if two loops link in the framework's sense, the ambient dimension D must be 3. The proof is a specialization: the general same-sector condition is D = 2p + 1, and setting p = 1 (loop-loop linking) gives D = 3.

The module also proves the converse for odd dimensions. For every odd D ≥ 3, it constructs an explicit witness: in R^(2p+1), two standard p-spheres in complementary position have linking number ±1. This gives a concrete example for each allowed dimension, not just an argument from parity. The allowed set A_A is characterized exactly: it consists of odd integers ≥ 3. The first few witnesses are D = 3 with p = 1, D = 5 with p = 2, D = 7 with p = 3, and D = 9 with p = 4.

These are formal theorems in the framework's machine-checked library of formal theorems. The loop-loop result is the topological specialization that supports the framework's claim that three spatial dimensions are forced. The converse witnesses show that the framework does not overreach: it permits odd dimensions beyond three for same-sector linking, but only the loop-loop case pins D to exactly 3.

The practical upshot is a precise boundary. The framework's dimension-forcing claim is not that all linking is three-dimensional; it is that the specific loop-loop configuration, the one that matches the framework's physical recognition-to-linking bridge, selects D = 3. The bridge itself, from physical recognition to topological linking, remains an open target, not a proved step.

/-- Loop-loop linking forces D = 3.
This is the (T) specialization: taking p = 1 in the same-sector
linking condition D = 2p+1 gives D = 3. -/
theorem loop_loop_linking_forces_D3 (D : ℕ) (h : D = 2 * 1 + 1) : D = 3 := by
  omega

/-- For odd D ≥ 3, D = 2 * witness_p D + 1. -/
theorem witness_reconstruction {D : ℕ} (hD : D ≥ 3) (hodd : ¬ 2 ∣ D) :
    D = 2 * witness_p D + 1 := by
  unfold witness_p
  omega

/-- The allowed-dimension set A_A consists exactly of odd integers ≥ 3.
Forward: if same-sector linking exists for some p ≥ 1, then D is odd ≥ 3.
Converse: for every odd D ≥ 3, witness_p provides the required p. -/
theorem allowed_set_A_characterization (D : ℕ) :
    (∃ p : ℕ, p ≥ 1 ∧ D = 2 * p + 1) ↔ (D ≥ 3 ∧ ¬ 2 ∣ D) := by
  constructor
  · rintro ⟨p, hp, hD⟩
    exact same_sector_forces_odd D p hp hD
  · rintro ⟨hD, hodd⟩
    exact ⟨witness_p D, witness_p_ge_one hD, witness_reconstruction hD hodd⟩

What this page does not claim

This module does not prove that physical space is three-dimensional; it proves a topological theorem about loop linking. The converse witnesses do not show that all odd dimensions are physically realized, only that they are topologically allowed.

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/Verification/DimensionLinking.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: