CohUnit
plain-language theorem explainer
CohUnit introduces an inductive type serving as the base dimension for coherence quantities inside the RS-native measurement scaffold. Workers building ledger observables or protocol-wrapped measurements cite it when constructing the Coh abbreviation. The declaration consists of a bare inductive definition with no constructors or proof obligations.
Claim. CohUnit is the inductive type of sort Type that supplies the unit for coherence quantities, where coherence quantities are formed as Quantity applied to this type.
background
The module supplies a Lean-first measurement scaffold for Recognition Science whose core theory remains RS-native: ticks, voxels, coherence (coh), action (act) and ledger observables, all normalized so that τ₀ = 1. SI/CODATA values are kept outside the core as optional external calibration. Protocols are required to be explicit so that windowing and coarse-graining choices cannot be hidden.
proof idea
The declaration is a bare inductive definition introducing the type CohUnit with no constructors or cases.
why it matters
CohUnit is used to form the abbreviation Coh := Quantity CohUnit, which anchors the coherence observable inside the RS-native measurement system. This supports the module goal of explicit protocols for every measurement and supplies the unit type required by downstream catalog entries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.