ActUnit
plain-language theorem explainer
The action unit type supplies the carrier for action quantities in the RS-native measurement system. Observables built on ledger quantities reference it when constructing action as a typed quantity. The declaration is introduced directly as an inductive type with no constructors or clauses.
Claim. Define the action unit type as an inductive type that serves as the base carrier for the action observable in the RS-native measurement framework.
background
The RS-native measurement framework supplies a Lean-first scaffold built from ticks, voxels, coherence, and action observables together with ledger quantities, fixing the base time scale at unity. External SI calibration is kept outside the core. This module remains dependency-light so that concrete observables can be added later in catalog files.
proof idea
The declaration is a direct inductive definition of the action unit type with no constructors supplied.
why it matters
The type feeds the action quantity definition used by all subsequent measurement constructions in the module. It enforces the design rule that every observable carries an explicit protocol, keeping arbitrary choices visible. It sits at the base of the RS measurement scaffold before any catalog observables are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.