pith. sign in
module module moderate

IndisputableMonolith.Physics.TopologicalChargesFromConfigDim

show as:
view Lean formalization →

The module defines topological charges and associated certificates derived from configuration dimension within the Recognition Science framework. Physicists modeling charge quantization from dimensional parameters would reference these objects when building topological invariants. The module consists entirely of definitions and certificates with no embedded proofs.

claimIntroduces TopologicalCharge, topologicalCharge_count, TopologicalChargesCert and topologicalChargesCert as functions and predicates on configuration dimension, building on the RS time quantum τ₀ = 1 tick.

background

The module imports IndisputableMonolith.Constants, whose sole documented content is the definition of the fundamental RS time quantum τ₀ = 1 tick. It introduces four sibling declarations that translate configuration dimension into discrete topological charges and certification structures. No further upstream theorems are referenced beyond this constant.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the core objects for expressing topological charge from configuration dimension. It sits at the base of any later physics constructions that require charge quantization in the Recognition Science setting, though 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)