momentum_raw
plain-language theorem explainer
The raw momentum conversion scales an RS-unit momentum value by the momentum quantum, which equals the coherence quantum under c=1. It is cited in RS-native calculations of particle momenta and conservation laws. The implementation is a single multiplication marked for simplification.
Claim. Let $p$ be a real number denoting momentum in the RS-native system. The raw momentum is defined as $p_{raw} = p · (E_{coh}/c)$, where $E_{coh}$ is the coherence quantum and $c=1$ in these units.
background
The RS-native units module establishes a measurement system based on the tick (time quantum) and voxel (spatial quantum), with derived quantities like the coherence quantum $E_{coh} = φ^{-5}$. Momentum is defined as an alias for the real numbers, allowing direct numerical representation. The momentum quantum is given by $E_{coh}/c$, which simplifies to $E_{coh}$ because the speed of light is unity in these units.
proof idea
This is a one-line definition that multiplies the input by momentumQuantum. No lemmas are applied beyond the definition of momentumQuantum.
why it matters
It provides the scaling for momentum in the RS-native system, supporting the overall constants module that defines all physical quantities in terms of the phi-ladder. This fits the framework's goal of expressing physics without external anchors, as described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.