pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Mathematics.KnotInvariantsFromRS

show as:
view Lean formalization →

The KnotInvariantsFromRS module defines knot invariants and certificates derived from Recognition Science. Mathematicians working on topological invariants linked to physical constants would cite it. The module consists of definitions for KnotInvariant, knotInvariant_count, KnotInvariantCert, and knotInvariantCert built directly on the imported RS time quantum.

claimDefines the knot invariant map $K: Knots → ℝ$ together with the counting function knotInvariant_count, the certificate type KnotInvariantCert, and the constructor knotInvariantCert, all parameterized by the RS time quantum τ₀ = 1 tick.

background

The module sits in the mathematics domain and imports only Mathlib plus IndisputableMonolith.Constants. The sole upstream dependency supplies the RS-native time quantum whose doc-comment states: 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.' Sibling declarations introduce the four objects KnotInvariant, knotInvariant_count, KnotInvariantCert, and knotInvariantCert that constitute the module's content.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the basic mathematical objects needed to express knot invariants inside the Recognition Science framework. It prepares the ground for later theorems that would connect these invariants to the unified forcing chain (T0–T8) and the Recognition Composition Law, although no downstream uses are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)