module module high

`IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan`

OptionAEmpiricalActionPlan specifies the coarse computational actions required to test a protocol under Option A in the Recognition Science foundation. It builds on the ordered schedule of the first five empirical tests from the upstream OptionAEmpiricalSchedule module. Researchers auditing empirical validation steps cite this module to identify required actions and their basic properties. The module consists of definitions and simple lemmas on actions rather than involved proofs.

claimThe coarse computational action $A$ needed to test a protocol, realized as an ordered sequence of high-or-immediate priority tests with explicit execution order and protocol coverage.

background

The module resides in the Foundation domain and imports OptionAEmpiricalSchedule. That upstream module fixes an explicit execution order for the first five empirical tests attached to Option A. It assigns priorities via the queue module and proves every scheduled item is high-or-immediate and protocol-covered.

This module defines the corresponding coarse computational actions. It introduces named actions (analysisAction, c3_action, c8_action and similar) together with predicates such as HasAnalysisAction and basic properties including counts and injectivity.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the action definitions that feed the OptionAEmpiricalDeliverables module, which converts the schedule into an auditable set of concrete outputs. It fills the empirical action-plan step in the foundation layer. The downstream module reports zero sorry and zero axiom.

scope and limits

Does not implement the individual test protocols.
Does not link to the forcing chain T0-T8 or RCL.
Does not derive constants or mass formulas.
Does not address Berry threshold or Z_cf values.

used by (1)

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

IndisputableMonolith.Foundation.OptionAEmpiricalDeliverables module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.OptionAEmpiricalSchedule module_import

declarations in this module (18)

inductive AnalysisAction L24
theorem analysisAction_count L36
def analysisAction L40
theorem analysisAction_injective L51
theorem c3_action L55
theorem c8_action L58
theorem c5_action L61
theorem c9_action L64
theorem c2_action L67
def HasAnalysisAction L71
theorem hasAnalysisAction_all L74
theorem scheduled_has_analysis_action L78
def firstPassActions L84
theorem firstPassActions_eq L87
theorem firstPassActions_length L97
theorem firstPassActions_nodup L102
structure EmpiricalActionPlanCert L107
def empiricalActionPlanCert L125