Quantity
plain-language theorem explainer
Quantity supplies the basic structure for real-valued observables tagged by a semantic unit type U inside the RS-native measurement system. Definitions of specific observables such as action or coherence cite it to keep unit labels distinct while inheriting real arithmetic. The declaration is a structure with one field together with instances that close the type under addition, negation, and scalar multiplication.
Claim. Let $U$ be any type. A quantity of label $U$ is the structure $Q = (v)$ with $v : ℝ$, together with the canonical coercion $Q → ℝ$ that extracts $v$.
background
The module supplies a Lean-first scaffold for Recognition Science measurements in which core observables remain RS-native (ticks, voxels, coherence, action) with $τ₀ = 1$ while SI calibration is kept external. Quantity is the uniform carrier for any real-valued ledger entry; its type parameter $U$ functions as the semantic tag that distinguishes, for example, action from cost. Upstream, the RS-native gauge $U$ from Constants.RSNativeUnits fixes $τ₀ = 1$ tick, $ℓ₀ = 1$ voxel and $c = 1$; the Recognition.U structure records recognition by structural equality.
proof idea
The declaration is a structure definition whose single field is val : ℝ. It is immediately followed by six instances that equip Quantity U with the operations of a vector space over ℝ: zero, addition, subtraction, negation and scalar multiplication, each implemented by delegating to the corresponding operation on the underlying real field.
why it matters
Quantity is the root type for the fourteen downstream aliases in the same module (Act, Coh, Cost, Meaning, Qualia, Skew and their companions). It therefore realizes the explicit-protocol measurement scaffold described in the module documentation and supplies the uniform real carrier needed for the RS-native constants, mass ladder and Berry threshold. In the larger framework it supports the forcing chain from T0 through T8 by keeping every observable tagged and algebraically closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.