TickUnit
plain-language theorem explainer
TickUnit is an empty inductive type that tags real-valued quantities as ticks in the RS-native measurement system. Modelers of discrete time steps or voxel observables in Recognition Science cite it when building Tick quantities from the Quantity structure. The declaration is a parameterless inductive with no constructors, serving solely as a semantic label.
Claim. Let $TickUnit$ be the inductive type with no constructors, used as a semantic tag $U$ so that a quantity is a structure containing a real number $val : ℝ$ labeled by this tag.
background
The module supplies a Lean-first scaffold for Recognition Science measurements in which every observable carries an explicit unit tag to keep protocols and falsifiers visible. Quantity $U$ wraps a real $val$ and inherits the standard ring operations via type-class instances. TickUnit is the empty tag type reserved for ticks, with the convention $τ_0 = 1$ fixed in the core theory.
proof idea
The declaration is a bare inductive definition introducing an empty type; no constructors, no tactics, and no proof obligations are present.
why it matters
TickUnit directly enables the downstream abbreviation Tick := Quantity TickUnit, which supplies the fundamental tick observable used throughout the RS measurement catalog. It implements the design goal of keeping core ticks (with $τ_0 = 1$) separate from optional SI calibrations and supports explicit protocol tracking for every measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.