pith. machine review for the scientific record. sign in
theorem proved decidable or rfl high

analysisAction_count

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

Lean usage

def empiricalActionPlanCert : EmpiricalActionPlanCert where nine_actions := analysisAction_count action_injective := analysisAction_injective c3_first_action := c3_action c8_second_action := c8_action c5_third_action := c5_action

formal statement (Lean)

  36theorem analysisAction_count : Fintype.card AnalysisAction = 9 := by

proof body

Decided by rfl or decide.

  37  decide
  38
  39/-- Action required by each implemented Option A combination. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.