Voxel
plain-language theorem explainer
Voxel supplies the native type for real-valued quantities labeled by the voxel unit in the RS measurement scaffold. Researchers deriving cone bounds, vacuum fractions, or running gravitational constants cite it when tagging lengths and densities at the recognition scale. The declaration is a direct one-line abbreviation that instantiates the Quantity structure with the VoxelUnit label.
Claim. A voxel quantity is a real number $q$ equipped with the voxel unit label, written $q : Q(U)$ where $Q$ is the structure attaching a real value to a semantic unit and $U$ is the inductive label for recognition voxels.
background
The module establishes an RS-native measurement framework whose core observables are ticks, voxels, coherence, and action with fundamental time scale set to one. Quantity is the structure that tags any real number with a unit label and supplies the coercion to reals together with the additive group operations. VoxelUnit is the inductive type that serves solely as the semantic tag distinguishing voxel quantities from other units such as time or cost.
proof idea
One-line abbreviation that directly aliases Quantity instantiated at VoxelUnit, inheriting the val field, zero, addition, subtraction, and real coercion from the Quantity definition.
why it matters
The abbreviation anchors all voxel-tagged observables that feed cone_bound_export (light-cone reach bounds), fractions_sum (passive plus active fraction equals one), voxel_density_scaling (effective voxel count versus radius), and the SI calibration maps to_meters and measure_to_meters. It realizes the RS-native measurement design in which SI conversion remains external while the eight-tick octave and phi-ladder scaling operate directly on voxel quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.