Skew
plain-language theorem explainer
Skew aliases a real-valued quantity carrying the SkewUnit label inside the RS-native measurement scaffold. Ledger algebra and Navier-Stokes modules cite it when encoding signed transfers or imbalances. The declaration is a direct one-line abbreviation of the Quantity structure.
Claim. A skew quantity is a real number equipped with the semantic label SkewUnit.
background
The RS-Native Measurement Framework supplies a Lean-first scaffold for core observables using ticks, voxels, and ledger quantities with τ₀ = 1. Quantity is the structure that tags any real value with a unit type and supplies zero, addition, subtraction, and coercion to ℝ. SkewUnit is the inductive tag type reserved for skew measurements. SI calibration remains external; all protocols and falsifiers stay explicit.
proof idea
The declaration is a one-line abbreviation that instantiates Quantity with the SkewUnit tag.
why it matters
Skew supplies the typed carrier for signed quantities inside MoralLedger, where agentSkew records net flux under the double-entry balance constraint σ = 0. It is invoked by the antisymmetry theorem for ledgerSkew and by the radial integral identity in SkewHarmGate. The abbreviation closes the measurement interface for Recognition Science ledger algebra and its Navier-Stokes extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.