IndisputableMonolith.Foundation.TopologicalConservation
Topological charges on an N-entry ledger are integer-valued configuration functionals invariant under variational dynamics. Integer codomain is structural charge quantization, not an extra postulate. Independent charge count equals three when D=3 and zero otherwise, via linking. Winding-charge and SM bookkeeping modules cite this layer. The file mixes definitions with dimension-case lemmas from DimensionForcing.
claimA topological charge on an $N$-entry ledger is a map $Q$ from configurations into $\mathbb{Z}$ invariant under the variational update. Charge quantization is the codomain $\mathbb{Z}$. The independent charge count is $3$ if spatial dimension $D=3$ and $0$ otherwise; linking of closed paths holds iff $D=3$. Standard-model charge labels sit on this integer lattice.
background
Recognition Science tracks ledger configurations under a discrete variational update (the missing equation of motion filled in VariationalDynamics). A topological charge is any integer-valued functional of the configuration that is constant along those trajectories. Integer-valuedness is the formal content of charge quantization: it is structural (codomain $\mathbb{Z}$), not imposed by hand.
DimensionForcing supplies the ambient fact that spatial dimension $D=3$ is forced, with a topological linking argument among its four routes. ParticleGenerations and InitialCondition sit nearby in the foundation stack (three fermion families; low-entropy start) but are imported mainly for shared ledger language.
The module therefore sits between forced geometry and conserved integer labels: once $D$ is fixed, the count of independent charges and the possibility of linking become sharp case distinctions rather than free parameters.
proof idea
Definitional core: TopologicalCharge as an integer configuration functional; zero and constant charges as trivial examples; quantization and trajectory conservation as immediate consequences of the $\mathbb{Z}$ codomain and invariance under the variational map; charge-at-any-tick as path-independence along discrete time.
Dimension casework: independent_charge_count is the piecewise rule (3 if $D=3$, else 0); three_charges_at_D3 and no_charges_at_other_D discharge the two branches; linking_iff_D3 and charge_count_equals_face_pairs connect the count to face-pair topology from DimensionForcing. SMCharge packages the standard-model labels on this integer lattice. No single deep induction: the force comes from the $D=3$ case split plus invariance by construction.
why it matters in Recognition Science
This module is the conservation layer of the foundation stack: it turns forced $D=3$ (T8 in the forcing chain) into a concrete integer charge count matching three independent SM-type charges. Downstream, WindingCharges imports it and supplies the missing mechanism: conservation laws arise from winding numbers of lattice paths. That module explicitly notes the piecewise definition independent_charge_count D := if D = 3 then 3 else 0 left implicit here and replaces the black box with winding.
Without this file, charge quantization and D-dependent charge count would remain informal. With it, later work can treat conserved integers as theorems about ledger trajectories rather than phenomenological inputs. It does not yet derive the full SM charge table from first principles; it only installs the topological integer scaffold those tables sit on.
scope and limits
- Does not derive the full Standard Model charge assignments from first principles.
- Does not prove conservation from winding; that mechanism is deferred to WindingCharges.
- Does not force D=3 itself; it consumes DimensionForcing.
- Does not address continuous gauge fields or Noether currents off the ledger.
- Does not claim nonzero charges exist for D other than 3.
used by (1)
depends on (4)
declarations in this module (27)
-
structure
TopologicalCharge -
theorem
topological_charge_quantized -
theorem
topological_charge_trajectory_conserved -
theorem
charge_at_any_tick -
def
zeroCharge -
def
constCharge -
def
independent_charge_count -
theorem
three_charges_at_D3 -
theorem
no_charges_at_other_D -
theorem
linking_iff_D3 -
theorem
charge_count_equals_face_pairs -
inductive
SMCharge -
theorem
sm_charge_count -
theorem
sm_charges_match_D3 -
def
charge_to_axis -
theorem
charge_to_axis_injective -
theorem
charge_to_axis_surjective -
theorem
charge_to_axis_bijective -
structure
NoetherCharge -
def
logChargeAsNoether -
def
topological_to_noether -
theorem
noether_not_necessarily_quantized -
def
addCharges -
def
negCharge -
theorem
total_charge_always_zero -
theorem
conservation_is_unconditional -
theorem
topological_conservation_certificate