Act
plain-language theorem explainer
Act is the native type for action quantities in Recognition Science, each carrying a real value tagged as one coherence-tick product. Calibration routines and Navier-Stokes hypotheses cite it when mapping RS observables to SI joule-seconds or when stating symmetry bridges. The declaration is a one-line abbreviation that specializes the generic Quantity structure to the ActUnit marker.
Claim. $Act := Quantity(ActUnit)$, where $Quantity(U)$ is the structure whose carrier is a real number equipped with semantic label $U$.
background
The RS-Native Measurement Framework treats action (act) as the product of one coherence and one tick with base time unit τ₀ = 1. Quantity is the structure that pairs any real value with a unit label and supplies the expected algebraic instances for zero, addition and subtraction. ActUnit is the empty inductive type that functions solely as the semantic tag distinguishing action from other observables such as length or time.
proof idea
One-line abbreviation that instantiates the Quantity structure on the ActUnit inductive type.
why it matters
Act supplies the domain for all downstream action-to-SI conversions, including to_joule_seconds and the theorem one_act_reports_hbar that recovers ħ. It is referenced by the narrativeTension_nonneg result and by the Quasi2DToComparisonSolutionHypothesis and Quasi2DToExactSymmetryHypothesis structures in the Navier-Stokes non-parasitism layer. The type therefore anchors the RS-native ledger before any external calibration is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.