MeaningUnit
MeaningUnit is the inductive type serving as the carrier for meaning units in the RS-native measurement system. It is referenced when defining quantities that embed explicit protocols and falsifiers for observables. The declaration is a bare inductive with no constructors, functioning as a type marker in the core scaffold.
claimLet $MeaningUnit$ be the inductive type that acts as the unit carrier for quantities in the Recognition Science measurement framework.
background
The module sets up a Lean-first scaffold for RS measurements where core observables are built from ticks, voxels, coherence, and action with $τ_0 = 1$. SI and CODATA values remain optional external calibration outside this core. Protocols must be carried explicitly so that windowing and coarse-graining choices cannot be hidden.
proof idea
The declaration is a bare inductive type definition with no constructors, serving directly as a type marker for use in Quantity.
why it matters in Recognition Science
MeaningUnit supplies the type parameter for the downstream abbreviation Meaning := Quantity MeaningUnit. This supports the module's design goal of protocol-explicit measurements within the RS-native ledger of ticks and voxels.
scope and limits
- Does not introduce any constructors or inhabitants.
- Does not state or prove any properties of the type.
- Does not connect to external SI calibration.
formal statement (Lean)
196inductive MeaningUnit : Type