analysisAction_count
plain-language theorem explainer
analysisAction_count establishes that the inductive type of coarse computational actions for Option A empirical tests has cardinality nine. Researchers implementing the Recognition Science empirical schedule would cite this to confirm the complete action inventory. The proof is a one-line decision procedure that enumerates the nine constructors of AnalysisAction.
Claim. The set of coarse computational actions needed to test a protocol has cardinality nine, where the set consists of the nine constructors fitFactorModel, fitDiscreteCollapse, plateauDetection, countRegulatoryStates, estimatePhiPowerRatio, trainMultiaxisDecoder, fitSharedResponseCoefficient, benchmarkCircuitAddressing, and orderProgressionTest.
background
The module defines concrete analysis action classes for the scheduled Option A empirical tests. The schedule determines the sequence of tests to run first, while this file specifies the kind of computation each test requires. AnalysisAction is the inductive type whose nine constructors enumerate the distinct tasks. Upstream results include the abbrev Action as real numbers from RSNativeUnits and the def A as active edge count per tick (equal to 1) from IntegrationGap, which satisfies the phi-power balance identity at D=3.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This succeeds because AnalysisAction is a finite inductive type with exactly nine constructors, making its Fintype.card decidable by direct enumeration and rfl.
why it matters
This theorem supplies the nine_actions field in the downstream empiricalActionPlanCert definition, which certifies the full Option A empirical action plan. It fills the requirement for a finite, enumerated set of computations in the Recognition Science framework, consistent with the eight-tick octave and the need for concrete tests on the phi-ladder. No open questions remain; the enumeration is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.