Status
plain-language theorem explainer
The declaration introduces the inductive type Status with four constructors spec, derived, hypothesis and scaffold, equipped with decidable equality and representation. Measurement theorists in the Recognition Science program cite it to tag how an observable is obtained from a state or trace. The definition is a direct inductive introduction with no lemmas or reductions required.
Claim. The inductive type classifying RS measurement status, with constructors spec (directly specified), derived (obtained from axioms), hypothesis (assumed) and scaffold (placeholder for later discharge), carrying decidable equality and a representation instance.
background
The RS-Native Measurement Framework (Core) module supplies a Lean-first scaffold for Recognition Science observables built from ticks, voxels, coherence and action, with fundamental period τ₀ = 1. SI/CODATA values remain outside the core as optional calibration. Every protocol is required to carry an explicit status tag together with falsifiers so that windowing or coarse-graining choices cannot be hidden. Status is the type that supplies these four tags. It draws on upstream definitions such as ArithmeticOf.extracted (arithmetic taken from a realization’s identity-step orbit) and IntegrationGap.A (active edge count per fundamental tick, fixed at 1).
proof idea
The declaration is introduced directly as an inductive type whose four constructors are listed explicitly, followed by the deriving clause for DecidableEq and Repr. No tactics, no lemmas and no reductions are applied; it is a pure data-type definition.
why it matters
Status supplies the classification used by the Action module theorems ground_state_is_unique_critical_point, principle_of_least_action, energy_conservation and energy_conservation_of_J_action, as well as by the astrophysics results AllConstantsDerived and H_RSZeroParameterStatus. It therefore anchors the measurement-protocol layer that feeds the variational principles and Noether theorems of the Recognition framework. The definition closes the explicit-protocol requirement stated in the module design goals and touches the open question of how hypothesis and scaffold constructors are eventually discharged by concrete theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.