pith. sign in
module module high

IndisputableMonolith.Foundation.TopologicalConservation

show as:
view Lean formalization →

The module defines topological charges on an N-entry ledger as integer-valued functions of configuration that remain invariant under the variational update map. Workers on conservation laws and the origin of quantized charges cite it to locate quantization in the codomain structure rather than an added postulate. The module assembles sibling definitions and lemmas that import D=3 forcing and the ledger dynamics to produce the integer codomain and the count of independent charges at D=3.

claimA topological charge is a map $q$ from ledger configurations to $\mathbb{Z}$ satisfying $q(\text{state}(t+1)) = q(\text{state}(t))$ under the variational dynamics; the codomain $\mathbb{Z}$ supplies quantization. At spatial dimension $D=3$ the module records exactly three independent such charges.

background

The module sits inside the Foundation layer after DimensionForcing (which forces $D=3$), VariationalDynamics (which supplies the state-to-state update rule), and ParticleGenerations. Its central object, TopologicalCharge, is an integer-valued function on configurations that is invariant under that update; the doc-comment states that integer-valuedness is the formal content of charge quantization and is structural rather than imposed.

Sibling declarations include topological_charge_quantized (the codomain claim), topological_charge_trajectory_conserved (invariance along trajectories), independent_charge_count (the function returning 3 when $D=3$ and 0 otherwise), three_charges_at_D3, no_charges_at_other_D, and linking_iff_D3. These rest on the upstream modules' statements that the ledger evolves by a fixed variational rule and that only $D=3$ permits nontrivial linking of paths.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the conservation statement that WindingCharges later equips with an explicit winding-number mechanism; the downstream doc-comment notes that TopologicalConservation left the mechanism implicit while already recording independent_charge_count $D :=$ if $D=3$ then 3 else 0. It therefore closes the step between variational dynamics and the three-generation structure at $D=3$ before the topological mechanism is supplied.

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)