Momentum
plain-language theorem explainer
Momentum is introduced as an alias for the real numbers in the RS-native units system. Researchers deriving conservation laws from space-translation invariance or constructing total Hamiltonians reference this when scaling momenta to the RS lattice. The declaration is a direct abbreviation with no computational content.
Claim. In the RS-native units with $c=1$, momentum is a real-valued quantity: $p : p$ takes values in the real numbers $p$.
background
The module defines an RS-native measurement system with tick as the atomic time quantum and voxel as the spatial step where light speed is unity. Derived quanta are the coherence energy $E_{coh} = phi^{-5}$ and action $hbar = E_{coh} cdot tau_0$. All quantities sit on the phi-ladder with dimensionless ratios fixed by phi alone.
proof idea
This declaration is a one-line abbreviation that identifies Momentum with the real numbers.
why it matters
This definition supports downstream constructions such as spaceTranslationFlow for momentum conservation and TotalHamiltonian over the voxel lattice. It aligns with the framework's requirement of three spatial dimensions and enables momentum_raw conversions in Noether theorems. It closes the interface for expressing conserved quantities in tick/voxel units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.