pith. machine review for the scientific record. sign in
structure definition def or abbrev high

TopologicalCharge

show as:
view Lean formalization →

Topological charge is an integer-valued map on N-entry configurations that stays fixed under any variational successor step. Researchers deriving conservation from topology in discrete systems rather than symmetries would cite this structure. The definition encodes quantization by codomain and invariance by the supplied predicate with no further proof steps required.

claimA topological charge on configurations of $N$ entries is a function $Q$ assigning an integer to each configuration such that $Q$ of the next configuration equals $Q$ of the current one whenever the next is a variational successor of the current.

background

A configuration is a tuple of $N$ positive real numbers serving as ledger entries. Variational successor is the update rule selecting the configuration of minimal total defect among those reachable under the dynamics. The module sets conservation as a topological invariant arising from linking in three dimensions, not from continuous symmetries, and contrasts it explicitly with Noether-type laws that need not be integer-valued.

proof idea

This is a structure definition that directly packages an integer-valued function with the invariance predicate. No lemmas or tactics are invoked; the codomain and the conserved field supply the entire content.

why it matters in Recognition Science

The structure supplies the common interface for all later results in the module, including unconditional conservation along trajectories and the construction of sums and negatives of charges. It realizes the F-012 claim that conservation laws originate from dimension-forced topology and feeds the downstream theorems that three independent charges exist precisely when the spatial dimension is three.

scope and limits

formal statement (Lean)

  64structure TopologicalCharge (N : ℕ) where
  65  value : Configuration N → ℤ
  66  conserved : ∀ (c next : Configuration N),
  67    IsVariationalSuccessor c next → value next = value c
  68
  69/-- **THEOREM (Quantization Is Automatic)**:
  70    Every topological charge takes integer values. -/

used by (17)

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

depends on (6)

Lean names referenced from this declaration's body.