pith. sign in
module module high

IndisputableMonolith.Foundation.TopologicalConservation

show as:
view Lean formalization →

TopologicalConservation defines topological charge as an integer-valued function on ledger configurations that stays fixed under the variational update rule. Workers on conservation laws and charge quantization in the Recognition framework cite it to ground integer quantization in the codomain rather than an added axiom. The module assembles definitions and basic invariance statements that link DimensionForcing's D=3 result to the winding-number mechanism developed downstream.

claimA topological charge is a map $C$ from ledger configurations to $ℤ$ such that $C$ is invariant under the variational dynamics map; the number of independent such charges equals 3 precisely when the spatial dimension is 3.

background

The module sits inside the Foundation layer and imports DimensionForcing (which forces D=3 via linking, self-similarity, and variational arguments), VariationalDynamics (which supplies the explicit state(t) to state(t+1) update rule), InitialCondition, and ParticleGenerations. Its central object is the integer-valued invariant function described in the module doc-comment: integer-valuedness supplies the formal content of charge quantization and is structural rather than imposed. Upstream DimensionForcing states that D=3 is forced by the RS framework through four arguments, one of which is topological linking.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the definition of topological charge and the count of independent charges at D=3 that WindingCharges consumes to replace the implicit placeholder with an explicit winding-number mechanism. It thereby closes the conservation-law gap noted in the downstream doc-comment and connects the D=3 forcing step to the later treatment of winding charges.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (27)