val_neg
plain-language theorem explainer
The theorem shows that negation of a quantity in the RS-native measurement system negates its underlying real value exactly. Researchers constructing arithmetic on signed observables or differences within Recognition Science would cite it to maintain consistency under the simp set. The proof is a direct reflexivity step once negation is defined componentwise on the real part.
Claim. For any unit label $U$ and real-valued quantity $a$, the real component of the negated quantity equals the negation of the original real component: $(-a).val = -a.val$.
background
The module supplies a Lean-first scaffold for RS measurements that keeps core theory native to ticks, voxels, and coherence with $τ_0=1$. Quantity is defined as a structure carrying a single real field val together with a semantic unit label $U$; it obtains Zero, Add, and Sub instances by lifting the corresponding operations on $ℝ$ directly to the val field. Upstream, RSNativeUnits.U fixes the gauge with $c=1$, while Recognition.U supplies the structural equality relation used for unit labels.
proof idea
The proof is a one-line reflexivity application. Negation on Quantity is realized by the Sub instance, which subtracts the real values componentwise, so the equality holds definitionally.
why it matters
This identity supplies the minimal algebraic hygiene required for signed quantities inside the RS measurement layer, ensuring that differences and directions remain compatible with real arithmetic. It supports the module's design goal of explicit protocols and falsifiers by keeping basic operations transparent. The result sits at the base of any later development that manipulates observables with sign, such as interval bounds or uncertainty propagation, while remaining independent of the phi-ladder or forcing-chain steps T5-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.