ZUnit
plain-language theorem explainer
ZUnit introduces the inductive base type for Z-quantities in the RS-native measurement scaffold. It is referenced when constructing observables such as ZCharge in the core framework. The declaration consists of a bare inductive type definition with no constructors or proof obligations.
Claim. Let $ZUnit$ be the inductive type that serves as the dimensional unit for Z-measurements.
background
The RS-Native Measurement Framework (Core) supplies a Lean-first scaffold for Recognition Science using ticks, voxels, coherence, action and ledger observables with τ₀ = 1. SI/CODATA values remain optional external calibration. The module keeps dependency light so that concrete observables can be added later in Catalog files. ZUnit supplies the unit type appearing in the sibling definition of ZCharge.
proof idea
The declaration is a direct inductive definition of the type ZUnit; the body contains no constructors and imposes no proof obligations.
why it matters
ZUnit supplies the unit type required by the downstream abbrev ZCharge := Quantity ZUnit. It therefore participates in the explicit-protocol design of the RS measurement system, ensuring every observable carries its protocol and falsifiers. The definition sits inside the core module whose goal is to keep all RS-native structure (ticks/voxels/ledger) inside Lean before any external calibration is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.