c3_action
plain-language theorem explainer
The theorem records that the oncology tensor combination maps to the fit factor model as its required analysis action. Researchers certifying the first-pass empirical schedule for Option A tests cite this equality to lock in the initial computation step. The proof is a direct reflexivity reduction from the defining clause of the analysisAction function.
Claim. analysisAction(c_3) = fitFactorModel, where c_3 is the oncology tensor combination and fitFactorModel is the corresponding analysis action type.
background
The module supplies concrete analysis action classes for the scheduled Option A empirical tests. The function analysisAction : CombinationID → AnalysisAction assigns to each implemented combination the computation it requires; its defining clause sends the oncology tensor case to fitFactorModel. This occurs inside the foundation layer that prepares the empirical pipeline, with zero sorrys or axioms present.
proof idea
The proof is a one-line reflexivity wrapper that matches the defining equation of analysisAction for the .c3OncologyTensor case.
why it matters
The equality supplies the c3_first_action field inside empiricalActionPlanCert, which in turn populates the EmpiricalPipelineCert structure used by the downstream pipeline certification. It therefore anchors the first scheduled test in the Option A empirical plan. While the surrounding framework derives physics from the forcing chain (T5 J-uniqueness through T8 D=3), this result is an implementation detail that ensures the concrete schedule begins with the fit factor model computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.