EmpiricalActionPlanCert
plain-language theorem explainer
EmpiricalActionPlanCert bundles the certification that the Option A plan uses nine analysis actions with an injective assignment function, maps c3OncologyTensor to fitFactorModel, c8MillerSpan to fitDiscreteCollapse and c5AttentionTensor to plateauDetection, and covers the first-pass schedule with five distinct actions. An auditor of the empirical test pipeline would reference this record to confirm the plan invariants. The declaration is a structure that simply enumerates these nine properties as fields.
Claim. Let $A$ be the inductive type of analysis actions. A certificate is a record asserting: $|A|=9$, the map $a: C → A$ is injective where $C$ is the type of implemented combinations, $a(c_3)=f$, $a(c_8)=d$, $a(c_5)=p$ for the designated actions $f,d,p$, every combination in the first-pass schedule $S$ satisfies $∃a∈A$ with $a(c)$ defined, the ordered list of first-pass actions equals $[f,d,p,r,e]$ with length 5 and no duplicates.
background
In the Option A empirical action plan module, AnalysisAction is the inductive type enumerating the coarse computational steps required to test each protocol: fitFactorModel, fitDiscreteCollapse, plateauDetection, countRegulatoryStates, estimatePhiPowerRatio and four further actions. The function analysisAction assigns to each CombinationID the required action; HasAnalysisAction c asserts that some action is assigned to combination c. The firstPassSchedule from the schedule module lists the initial five combinations to test in order.
proof idea
This is a structure definition that packages nine independent properties into a single record type. The fields nine_actions, action_injective, c3_first_action, c8_second_action, c5_third_action, scheduled_actions, first_pass_actions, first_pass_actions_length and first_pass_actions_nodup are simply asserted as the structure fields; no tactics or lemmas are applied because the declaration is a pure record constructor.
why it matters
The certificate is instantiated in the downstream definition empiricalActionPlanCert, which supplies concrete proofs for each field using lemmas such as analysisAction_count, analysisAction_injective, c3_action, c8_action and c5_action. It anchors the empirical validation track of Option A by ensuring the first-pass schedule is fully covered by distinct actions before any data collection begins. Within the Recognition Science framework this supplies the concrete computational requirements for the initial empirical tests that probe the phi-ladder and J-cost relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.