Act
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 in Recognition Science
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.
scope and limits
- Does not assign a numerical conversion factor to SI units.
- Does not enforce positivity or boundedness on values.
- Does not encode measurement protocols or uncertainty intervals.
- Does not define addition or multiplication beyond the inherited Quantity instances.
formal statement (Lean)
203abbrev Act := Quantity ActUnit