val_add
plain-language theorem explainer
Addition of two RS-native quantities preserves the underlying real value by construction. Researchers composing measurements in pattern recognition or cycle algorithms cite this when verifying additive closure. The proof is immediate reflexivity from the Add instance on the Quantity structure.
Claim. For quantities $a$ and $b$ of the same unit type $U$, the real value of their sum equals the sum of their values: $val(a + b) = val(a) + val(b)$.
background
The RS-native measurement framework defines a Quantity as a real number tagged by a semantic unit type $U$, with addition implemented by direct summation on the val field. This core module establishes the native gauge with $τ_0 = 1$ tick and $ℓ_0 = 1$ voxel, keeping SI calibration external. Upstream, the U definition from RSNativeUnits supplies the gauge constants while the Recognition.U structure enforces recognition by structural equality.
proof idea
The proof is a one-line reflexivity that unfolds the Add instance for Quantity, which constructs the sum quantity directly from the sum of the val components.
why it matters
This supports downstream results including roots_form_group in the imaginary unit module and brgc_oneBit_step in Gray cycle patterns by guaranteeing additive composition of quantities. It anchors the measurement scaffold in the RS framework, where observables carry explicit protocols and tie into the T0-T8 forcing chain via native units. It closes a basic interface for later pattern and recognition lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.