Meaning
plain-language theorem explainer
Meaning supplies the semantic type for real-valued quantities carrying the MeaningUnit label inside the RS-native measurement scaffold. Researchers constructing vantage categories or physics observables cite it when tagging states in the outside vantage. The declaration is a direct one-line abbreviation that instantiates the generic Quantity structure on the marker type MeaningUnit.
Claim. Let $Meaning$ denote the type of real-valued quantities equipped with the semantic marker $MeaningUnit$, where $Quantity(U)$ is the structure whose carrier is a real number $val$ together with the usual additive group operations and coercion to $ℝ$.
background
Quantity is the structure that wraps a real number $val$ and equips it with zero, addition, subtraction, and coercion to $ℝ$, thereby tagging any numerical datum with a unit type $U$. MeaningUnit is an empty inductive type whose sole purpose is to serve as that semantic label. The module sets the local theoretical setting for an RS-native measurement framework in which every observable is carried by a tagged quantity, with $τ₀ = 1$ and all protocols kept explicit before any external calibration is introduced.
proof idea
The declaration is a one-line abbreviation that directly instantiates Quantity with the MeaningUnit marker type.
why it matters
This abbreviation supplies the concrete type used inside the outsideVantage definition, which models the Physics vantage containing geometry, energy, and observables. It therefore sits at the root of the VantageCategory construction and supports the module's design goal of keeping core theory RS-native. No open question is closed by this alias; it simply provides the typed carrier required by downstream vantage definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.