val_smul
plain-language theorem explainer
The theorem states that scalar multiplication of a real-valued quantity by a real scalar r acts componentwise on the underlying numerical value. Researchers building RS-native measurement protocols would cite it when reducing expressions that scale observables tagged by unit labels. The proof is a one-line reflexivity that follows directly from the definition of scalar multiplication on the Quantity structure.
Claim. Let $r$ be a real number and let $a$ be a real-valued quantity labeled by a unit type $U$. Then the value of the scaled quantity satisfies $val(r · a) = r · val(a)$.
background
The RS-Native Measurement Framework supplies a Lean-first scaffold for Recognition Science observables built from ticks, voxels, and ledger entries with $τ₀ = 1$. A Quantity is a real number equipped with a semantic unit label $U$, together with the standard real addition, subtraction, and scalar-multiplication instances. The local setting treats SI/CODATA values as optional external calibration while keeping core arithmetic RS-native.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of scalar multiplication on Quantity.
why it matters
This simp theorem supplies the basic algebraic reduction rule for scaled quantities inside the core measurement module. It supports consistent simplification of expressions that appear in RS-native protocols and ledger observables. The result sits under the RS-native gauge $U$ (with $τ₀ = 1$, $ℓ₀ = 1$, $c = 1$) and prepares the ground for later catalog definitions of concrete observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.