RSUnits
plain-language theorem explainer
RSUnits packages the core RS-native units as real numbers tau0 for the tick duration, ell0 for the voxel length, and c for speed, together with the enforced relation c tau0 equals ell0. Certificate and display authors in the Constants and Certificates modules cite this structure to keep scaling consistent. The declaration is introduced as a direct structure definition whose fields embed the light-cone identity without further lemmas.
Claim. A structure consisting of real numbers $tau_0$, $ell_0$, $c$ satisfying $c cdot tau_0 = ell_0$, where $tau_0$ is the fundamental time quantum equal to one tick and $ell_0$ is the fundamental length unit.
background
The Constants module defines the fundamental RS time quantum as tau0 equal to one tick and sets ell0 to 1 in native units. The speed c is fixed by the upstream light-cone lemma c_ell0_tau0 that asserts ell0 equals c times tau0. This structure collects the three quantities and their relation into a single package for use in bridges and ratio computations. The sibling definition K equals the square root of phi supplies the dimensionless bridge ratio referenced alongside these units.
proof idea
This is a structure definition that directly declares the four fields tau0, ell0, c as real numbers and c_ell0_tau0 as the equality c times tau0 equals ell0. No tactics, lemmas, or reductions are applied; the relation is part of the structure signature itself.
why it matters
RSUnits supplies the unit package referenced by UnitsKGateCert, computeRatios, and the display theorems display_null_condition and display_rate_matches_structural_rate. It anchors the constants used in ConeEntropyFacts and KDisplay results, supporting consistent scaling for the recognition framework and its dimensionless bridge K. The definition closes the core interface for unit traceability in the Constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.