module module high

`IndisputableMonolith.Foundation.TopologicalConservation`

TopologicalConservation defines topological charges as integer-valued functions on ledger configurations that stay invariant under the variational dynamics update. Charge quantization is structural because the codomain is the integers. Researchers tracing conservation laws from dimension forcing to winding mechanisms cite it when building the topological layer of the Recognition Science ledger. The module supplies definitions and basic invariance statements that later modules extend.

claimA topological charge on an $N$-entry ledger is a map $Q$ from configurations to integers such that $Q$ is invariant under the variational dynamics transition: $Q(s(t+1)) = Q(s(t))$.

background

The module sits inside the Recognition Science ledger formalism. Configurations evolve by the state transition map supplied by the imported VariationalDynamics module. It inherits the forced spatial dimension $D=3$ from DimensionForcing (via its topological linking argument), the low-entropy initial condition, and the three fermion generations. The supplied doc-comment states that integer-valuedness is the formal content of charge quantization and is structural rather than imposed.

proof idea

This is a definition module, no proofs. It introduces the TopologicalCharge type together with predicates such as topological_charge_quantized and topological_charge_trajectory_conserved, constant and zero constructions, and the count independent_charge_count that equals 3 precisely when $D=3$.

why it matters in Recognition Science

The module supplies the definitions that WindingCharges extends by replacing the implicit conservation statement with an explicit winding-number mechanism. It closes the topological step between DimensionForcing (T8: $D=3$) and the conservation laws required for the full RS framework. The downstream doc-comment notes that the earlier definition independent_charge_count $D :=$ if $D=3$ then 3 else 0 is now given a concrete topological realization.

scope and limits

Does not construct explicit non-constant charges.
Does not prove invariance outside the variational update rule.
Does not derive the numerical value 3 from first principles.
Does not connect charges to the phi-ladder or mass formulas.
Does not address quantization in dimensions other than 3.

used by (1)

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

IndisputableMonolith.Foundation.WindingCharges module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.VariationalDynamics module_import

declarations in this module (27)

structure TopologicalCharge L64
theorem topological_charge_quantized L71
theorem topological_charge_trajectory_conserved L76
theorem charge_at_any_tick L85
def zeroCharge L94
def constCharge L99
def independent_charge_count L111
theorem three_charges_at_D3 L114
theorem no_charges_at_other_D L117
theorem linking_iff_D3 L122
theorem charge_count_equals_face_pairs L127
inductive SMCharge L133
theorem sm_charge_count L139
theorem sm_charges_match_D3 L141
def charge_to_axis L146
theorem charge_to_axis_injective L151
theorem charge_to_axis_surjective L154
theorem charge_to_axis_bijective L160
structure NoetherCharge L166
def logChargeAsNoether L172
def topological_to_noether L177
theorem noether_not_necessarily_quantized L185
def addCharges L212
def negCharge L217
theorem total_charge_always_zero L223
theorem conservation_is_unconditional L231
theorem topological_conservation_certificate L249