Foundation Linking Numbers

Linking Numbers

Linking numbers are a topological invariant that counts how many times one closed curve winds around another. In Recognition Science, they are defined on pairs of closed paths in a D-dimensional integer lattice. The module LinkingNumbers.lean formalizes this concept and proves the key results that connect topology to conservation.

The central theorem, linking_gives_conservation, establishes that in three dimensions, linked pairs of closed paths exist, their linking numbers are integers, and there are exactly three independent charges. This is the concrete topological invariant that supports the claim that D = 3 allows non-trivial linking, a step beyond the winding numbers of single paths.

The module proves that an explicit linked pair, the Hopf link, exists in D = 3 (hopf_link_exists_D3), and that its linking number is 1 (hopf_linking_number). It also proves that in one dimension, all closed paths have zero winding number (D1_all_closed_trivial), so no non-trivial linking is possible. The summary theorem linking_dimension_summary states that D = 1 has no independent loops, D = 2 has one loop but no linking, and D = 3 has three loops with linking.

The linking number is invariant under local deformations that cancel pairs of steps (linking_preserved_under_deformation). This invariance is what makes it a true topological invariant, not just an artifact of a particular path representation. The existence of this invariant in D = 3 is what forces the physical dimension to be three, as stated in linking_dimension_summary.

THEOREM linking_gives_conservation · IndisputableMonolith/Foundation/LinkingNumbers.lean

THEOREM hopf_link_exists_D3 · hopf_linking_number · IndisputableMonolith/Foundation/LinkingNumbers.lean

THEOREM D1_all_closed_trivial · IndisputableMonolith/Foundation/LinkingNumbers.lean

THEOREM linking_dimension_summary · IndisputableMonolith/Foundation/LinkingNumbers.lean

THEOREM linking_preserved_under_deformation · IndisputableMonolith/Foundation/LinkingNumbers.lean

What this page does not claim

This answer does not claim that linking numbers are the only topological invariant needed for conservation. This answer does not claim that the physical recognition-to-linking bridge is established; it remains open. This answer does not claim that linking numbers are defined for continuous curves, only for lattice paths.

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/LinkingNumbers.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: