Skew
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assign numerical values or conversion factors to skew quantities.
- Does not impose algebraic relations beyond those inherited from Quantity.
- Does not connect skew to the phi ladder or any specific physical constants.
formal statement (Lean)
205abbrev Skew := Quantity SkewUnit