Mathematics Knot Invariants From Rs

Five knot invariants

Knot theory asks when two tangled loops are the same. A knot invariant is a quantity or algebraic object assigned to a knot that does not change under continuous deformation, so if two knots have different invariants, they are genuinely different. The classical families include the genus, the minimum crossing number, the Alexander polynomial, the Jones polynomial, and Khovanov homology. Each one sees structure the others miss: the Alexander polynomial captures abelian coverings, the Jones polynomial comes from quantum groups and braid representations, and Khovanov homology upgrades the Jones polynomial to a graded homology theory that distinguishes knots the polynomial alone cannot.

The subject developed over more than a century. Peter Guthrie Tait tabulated knots by crossing number in the 1870s and 1880s, and J. W. Alexander introduced his polynomial in 1928. Vaughan Jones discovered his polynomial in 1984 while working on operator algebras, and Mikhail Khovanov defined his homology in 2000. These five families are not arbitrary: they form a ladder of increasing discrimination. Genus is a coarse topological measure, crossing number is combinatorial, the Alexander polynomial is algebraic, the Jones polynomial is stronger, and Khovanov homology is the finest of the five. No single invariant is complete, and the search for complete invariants remains open.

In Recognition Science, the framework models knot-type discrimination as a discrete recognition process. Its machine-checked library of formal theorems defines an inductive type with exactly these five invariants as constructors, and proves that the cardinality of this type is five. The proof is a direct computation: the type has five elements, and the library checks the count with no axioms beyond the standard logical ones and no unfinished proofs. The certificate structure packages this fact, so the count is available as a reusable theorem.

The framework's contribution is not a new knot invariant. It is a structural claim: these five families form a closed set under the framework's notion of recognition cost. The library proves the count, not the discrimination power of any individual invariant. The classical theory of knot invariants remains the source of their definitions and properties; the framework adds a formal account of why these five, and not others, appear as the canonical ladder.

What this changes is the status of the list. Instead of a historical accident or a convenient collection, the five families become a proved structural unit within the framework. The count is verified by machine, so a reader can trust the number five without checking the enumeration by hand. The framework does not prove that these invariants are complete or that no other invariant exists; it proves that its own model of knot-type discrimination contains exactly these five.

inductive KnotInvariant where
  | genus
  | crossingNumber
  | alexanderPoly
  | jonesPoly
  | khovanovHomology
  deriving DecidableEq, Repr, BEq, Fintype

theorem knotInvariant_count : Fintype.card KnotInvariant = 5 := by decide

def knotInvariantCert : KnotInvariantCert where
  five_invariants := knotInvariant_count

What this page does not claim

The framework does not prove that these five invariants are complete or that no other knot invariant exists. The framework does not derive the definitions or properties of the individual invariants from recognition cost. The count of five is a theorem about the framework's model, not a claim that classical knot theory has exactly five invariants.

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/Mathematics/KnotInvariantsFromRS.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: