constCharge
The declaration builds a topological charge that returns the fixed integer n for every configuration on an N-entry ledger. Researchers modeling quantized invariants in the Recognition Science ledger cite it when constructing trivial conserved quantities independent of dynamics details. The construction is a direct structure definition that sets the value map to the constant function and confirms invariance by reflexivity on the successor predicate.
claimFor natural number $N$ and integer $n$, the constant topological charge is the structure whose value map sends every configuration to $n$ and whose conservation property holds identically under any variational successor.
background
The module establishes that conservation laws in Recognition Science originate from topological linking in dimension 3 rather than continuous symmetries. TopologicalCharge is the structure consisting of an integer-valued function on configurations together with the requirement that this function is invariant under the variational successor relation. The module imports DimensionForcing to enforce D=3 as the unique dimension permitting nontrivial linking and uses the ledger factorization from DAlembert to ground the dynamics.
proof idea
The definition constructs the TopologicalCharge record by assigning the constant function returning n to the value field and discharging the conserved field with the reflexivity tactic on the equality of integers.
why it matters in Recognition Science
It supplies the simplest example of a quantized topological charge, supporting the module's enumeration of independent charges at D=3 and the contrast with Noether charges that need not be integers. The parent results include three_charges_at_D3 and topological_charge_quantized, which rely on the existence of such constant instances to count linking numbers per coordinate plane of Q3.
scope and limits
- Does not derive the integer n from any linking number or configuration data.
- Does not enforce the D=3 restriction or count independent charges.
- Does not connect the constant to physical quantities such as baryon or lepton number.
- Does not address time evolution beyond the successor invariance.
formal statement (Lean)
99def constCharge (N : ℕ) (n : ℤ) : TopologicalCharge N where
100 value := fun _ => n
proof body
Definition body.
101 conserved := fun _ _ _ => rfl
102
103/-! ## Part 3: Charge Count from Dimension -/
104
105/-- The number of **independent topological charges** supported by dimension D.
106
107 - D = 1: 0 (no linking)
108 - D = 2: 0 (everything unlinks)
109 - D = 3: 3 (one per coordinate plane of Q₃)
110 - D ≥ 4: 0 (everything unlinks) -/