analysisAction
plain-language theorem explainer
analysisAction supplies the analysis procedure assigned to each Option A combination. It is cited by any proof that needs to know what computation validates a given protocol. The definition is a direct case split on the CombinationID constructors with no additional lemmas.
Claim. The mapping from implemented Option A combinations to required analysis actions is given by cases: oncology tensor combination maps to factor model fit, Miller span to discrete collapse fit, attention tensor to plateau detection, regulatory ceiling to regulatory state count, planet strata to phi power ratio estimate, cognitive tensor to multiaxis decoder training, universal response to shared response coefficient fit, quantum molecular depth to circuit addressing benchmark, and Erikson reverse to progression order test.
background
The module Option A Empirical Action Plan supplies concrete analysis action classes for the scheduled Option A empirical tests. The schedule determines the order of tests; this definition specifies the kind of computation each test requires. AnalysisAction is the inductive type whose constructors name the coarse computational actions needed to test a protocol: fitFactorModel, fitDiscreteCollapse, plateauDetection, countRegulatoryStates, estimatePhiPowerRatio, trainMultiaxisDecoder, fitSharedResponseCoefficient, benchmarkCircuitAddressing, and orderProgressionTest. CombinationID, imported from the falsifier registry, enumerates the implemented Option A combinations: c1CognitiveTensor through c9RegulatoryCeiling, with c10 left as commentary.
proof idea
The definition proceeds by pattern matching on the nine constructors of the CombinationID inductive type, returning the corresponding AnalysisAction constructor in each case. No lemmas are applied; the mapping is given directly by the cases.
why it matters
This definition is invoked by the injectivity theorem analysisAction_injective and by the specific action theorems such as c2_action, c3_action, and c5_action that record the value for each combination. It completes the specification of the empirical action plan for Option A, linking the scheduled tests to the required computational procedures in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.