MeaningUnit
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.