momentumQuantum
plain-language theorem explainer
Momentum quantum is defined as the coherence energy quantum divided by the speed of light in RS-native units. Researchers scaling momenta on the phi-ladder cite this definition when working in the tick-voxel system. The definition is a direct abbreviation that applies the prior cohQuantum value under the c=1 convention.
Claim. The momentum quantum is $p_Q := E_c / c$ where $E_c = phi^{-5}$ is the coherence energy quantum and $c = 1$ in RS units.
background
The RSNativeUnits module sets up a native measurement system with tick as the atomic time interval and voxel as the spatial step where light travels in one tick. Derived units include the coherence quantum E_coh = phi^{-5} and action quantum equal to E_coh times the tick. All scales follow the phi-ladder with c fixed at unity. This definition draws on the upstream cohQuantum which sets the energy quantum to phi^{-5} and the scale function that computes phi^k steps.
proof idea
One-line wrapper that applies division of cohQuantum by c with the simp attribute attached for automatic reduction.
why it matters
This supplies the scaling factor for momentum in the native system and feeds momentum_raw which multiplies a Momentum value by the quantum. It also supports the downstream equality lemma that reduces momentumQuantum to cohQuantum under c=1. The step aligns with the phi-ladder organization and the framework constants where c=1 and energies sit at phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.