ZCharge
plain-language theorem explainer
ZCharge is the abbreviation for real-valued quantities carrying the ZUnit semantic label. It supplies the native type for charge observables inside the RS measurement scaffold. Modelers of ledger charge in terms of recognition ticks reference this when building protocol-tagged entries. The declaration is a direct one-line abbreviation with no computational obligations.
Claim. Let $ZCharge$ denote the type of real numbers equipped with the semantic unit label $ZUnit$.
background
The RS-Native Measurement Framework (Core) supplies a Lean-first scaffold for observables built from ticks, voxels, and ledger entries with $τ₀ = 1$. Quantity is the structure that wraps a real value with a unit type parameter, providing coercion to ℝ together with the usual additive group operations. ZUnit is the empty inductive type that functions purely as a semantic tag for charge. Upstream Measurement structures from Data.Import and the local module add protocol, optional window, and uncertainty fields to any such quantity.
proof idea
The declaration is a direct one-line abbreviation that instantiates Quantity with ZUnit.
why it matters
ZCharge fixes the native unit for charge inside the RS measurement core, keeping SI calibration outside the foundational layer. It supports later catalog definitions of charge observables while preserving explicit protocols. No immediate dependents appear in the current graph, leaving its use open for downstream ledger constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.