Charge
plain-language theorem explainer
Charge supplies the real-valued type for electric charge in the RS-native unit system. Topological conservation and winding charge results cite it to assign values to lattice configurations and trajectories. The declaration is a direct abbreviation to the reals with no additional structure or lemmas.
Claim. Charge denotes the real line $ℝ$ as the codomain for charge assignments on configurations in the Recognition Science lattice.
background
The RSNativeUnits module defines a native measurement system whose base is the tick τ₀ = 1, the fundamental time quantum, together with the voxel as the corresponding spatial step. Derived quantities include the coherence quantum coh = φ^{-5} and the action quantum act = ħ. All dimensionless ratios are fixed by φ, and c = 1 holds by construction. Charge is introduced here as the real type that receives values from winding numbers and topological charges. Upstream, the tick definition states τ₀ = 1 and notes that one octave equals eight ticks, supplying the discrete time base used throughout the ledger.
proof idea
The declaration is a one-line abbreviation Charge := ℝ. No lemmas or tactics are invoked; the alias simply re-exports the real numbers for subsequent charge constructions.
why it matters
Charge supplies the codomain used by constCharge, topological_charge_trajectory_conserved, and winding_charges_certificate. These results establish that winding numbers are additive integers that yield conserved charges precisely when D = 3, matching the eight-tick octave and the forced spatial dimension T8. The definition therefore closes the interface between lattice windings and real-valued Noether charges without requiring quantization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.