Velocity
plain-language theorem explainer
Velocity is the type for speeds expressed in voxels per tick under the RS-native unit system with c fixed at unity. It is cited in fluid Galerkin expansions, discrete Navier-Stokes operators, and classical limits of quantum emergence. The declaration is a direct type abbreviation to the reals carrying no further axioms or reductions.
Claim. In the RS-native units, velocity is an element of the real numbers $ℝ$.
background
The RS-native measurement system defines tick (τ₀) as one discrete ledger posting interval and voxel (ℓ₀) as the causal spatial step traversed by light in one tick. Derived quanta are coh (energy quantum φ⁻⁵) and act (action quantum ħ = E_coh · τ₀). All velocities are therefore dimensionless ratios in voxel/tick units, with the speed of light satisfying c = 1 by construction. The φ-ladder supplies the natural scaling for masses, energies, and lengths throughout the framework.
proof idea
The declaration is a direct abbreviation to the real number type; no lemmas or tactics are applied.
why it matters
Velocity supplies the codomain for the canonical speed c := 1 and appears in the NewtonianParticle structure and in total_conservativeTransportField_zero. It anchors the c = 1 convention required by the T0-T8 forcing chain and the Recognition Composition Law. The type is referenced by SPARC falsifiers and Galerkin2D mode spaces, closing the bridge from ledger primitives to classical hydrodynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.