Pith. sign in
module module low

IndisputableMonolith.Mathematics.KnotInvariantsFromRS

show as:
view Lean formalization →

This module introduces definitions for knot invariants derived from Recognition Science. Mathematicians exploring topological structures in RS-derived physics would cite it. The module consists of definitions building directly on the imported RS constants module.

claimThe module defines $\text{KnotInvariant}$ and $\text{KnotInvariantCert}$ as RS-derived objects on knots, together with counting functions $\text{knotInvariant_count}$ and certification predicates.

background

The module imports Mathlib for standard mathematical structures and IndisputableMonolith.Constants. The Constants module supplies the fundamental RS time quantum $\tau_0 = 1$ tick. No further definitions or theorems are supplied in the module header; the listed sibling declarations establish the main objects.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the mathematical objects needed to express knot invariants inside the Recognition Science framework. It sits downstream of the Constants module and provides tools that later results in the mathematics domain can reference when linking RS to topology.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)