val_zero
plain-language theorem explainer
The zero element of the Quantity structure projects to the real number zero under its val field. Measurement and forcing-chain authors cite this when normalizing additive identities in RS-native observables or applying simp in ledger and curvature calculations. The proof is immediate reflexivity on the Zero instance definition.
Claim. For any type $U$, the valuation of the zero quantity satisfies $val(0_U) = 0$.
background
Quantity is a structure that pairs a real number val with a semantic unit label U, equipped with a Zero instance that constructs the element as ⟨0⟩. The module supplies an RS-native measurement scaffold in which observables are built from ticks and voxels with τ₀ = 1 and c = 1, as supplied by the RSUnits gauge in Constants.RSNativeUnits. This identity is the additive zero property required before any protocol or ledger operation can be stated.
proof idea
The proof is a one-line wrapper that applies reflexivity (rfl) directly to the Zero instance for Quantity U, where zero is defined as ⟨0⟩ and val extracts the inner real number.
why it matters
The result anchors the core measurement layer that feeds modularRealization in UniversalForcing and the Riemann symmetry lemmas in Relativity.Geometry. It supplies the additive identity inside the RS-native units where τ₀ = 1, closing the basic arithmetic needed for forcing-chain realizations and curvature identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.