empiricalActionPlanCert
plain-language theorem explainer
This definition assembles the complete certificate for the Option A empirical action plan by instantiating the required structure with verified properties of the analysis actions. Researchers verifying scheduled empirical tests in the Recognition Science foundation would cite it to confirm that the nine actions, their injectivity, and specific mappings satisfy the plan. The construction is a direct structure fill that references sibling theorems for cardinality, injectivity, and action correspondences.
Claim. The empirical action plan certificate is the structure whose fields satisfy: the cardinality of analysis actions equals 9, the mapping from combinations to actions is injective, the c3 oncology tensor maps to the fit factor model, the c8 Miller span maps to discrete collapse, the c5 attention tensor maps to plateau detection, every combination in the first-pass schedule has an analysis action, the first-pass actions equal the listed sequence of models, their length is 3, and they contain no duplicates.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The imported schedule determines test order while this file specifies the computational type required for each test. The central definition is the structure EmpiricalActionPlanCert whose fields bundle the nine-action count, injectivity of the action map, and explicit correspondences such as c3OncologyTensor to fitFactorModel.
proof idea
The definition is a direct structure construction that assigns each field to the corresponding sibling result: nine_actions receives the cardinality theorem, action_injective receives the case-analysis injectivity proof, c3_first_action receives the reflexivity equality for c3, and likewise for the remaining fields including the schedule predicate and first-pass list properties.
why it matters
This definition supplies the top-level certificate that closes the Option A action-plan implementation inside the foundation layer. It assembles the concrete computational requirements that support empirical validation steps in the Recognition Science framework, particularly those tied to the forcing chain and phi-ladder mass formulas. No downstream theorems yet reference it, leaving open its integration into larger schedule-verification results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.