pith. machine review for the scientific record. sign in
def definition def or abbrev high

empiricalProgramCert

show as:
view Lean formalization →

The declaration supplies a concrete certificate assembling all metadata properties of the first-pass empirical program for Option A. Researchers validating the Recognition Science empirical layer would cite it as the single reference object for program completeness and collision-freeness. The definition is a direct record construction that wires each field to a previously established lemma.

claimLet $EmpiricalProgramCert$ be the structure whose fields require that $programSpec$ is injective, the first-pass program has length 5 and contains no duplicates, satisfies readiness and completeness, the schedule meets readiness and pipeline conditions for every combination, action and deliverable classes are duplicate-free, pipeline records are duplicate-free, and the schedule selects precisely the high-or-immediate priorities. Then $empiricalProgramCert$ is the instance of this structure obtained by assigning each field the corresponding proved fact.

background

The module OptionAEmpiricalProgram constructs a single certificate for the first-pass empirical program attached to Option A. The structure $EmpiricalProgramCert$ collects the required properties: injectivity of $programSpec$, length of $firstPassProgram$ equal to 5, absence of duplicates in the program list, readiness via $FirstPassReady$, completeness via $FirstPassProgramComplete$, scheduled readiness and pipeline conditions, no duplicates among action classes, deliverable classes, and pipeline records, and exact selection of top-priority items.

proof idea

The definition is a record constructor that directly assigns each field of $EmpiricalProgramCert$ to the corresponding theorem: $program_injective$ to $programSpec_injective$, $first_pass_length$ to $firstPassProgram_length$, $first_pass_nodup$ to $firstPassProgram_nodup$, $first_pass_ready$ to $firstPassReady$, $first_pass_complete$ to $firstPassProgramComplete$, and the remaining nodup and priority fields to their respective lemmas.

why it matters in Recognition Science

This declaration supplies the assembled certificate for the Option A empirical program, serving as the single reference point for the first-pass test suite. The module documentation states that the file proves the assembled first-pass program is complete and collision-free at the metadata layer. It closes the empirical readiness assembly step within the Recognition framework, though no downstream uses are recorded yet.

scope and limits

formal statement (Lean)

 127def empiricalProgramCert : EmpiricalProgramCert where
 128  program_injective := programSpec_injective

proof body

Definition body.

 129  first_pass_length := firstPassProgram_length
 130  first_pass_nodup := firstPassProgram_nodup
 131  first_pass_ready := firstPassReady
 132  first_pass_complete := firstPassProgramComplete
 133  scheduled_ready := scheduled_program_ready
 134  scheduled_pipeline := scheduled_program_pipeline
 135  action_classes_nodup := firstPassProgram_actions_nodup
 136  deliverable_classes_nodup := firstPassProgram_deliverables_nodup
 137  pipeline_records_nodup := firstPassProgram_pipelines_nodup
 138  exact_top_priority := firstPassProgram_exact_top_priority
 139
 140end OptionAEmpiricalProgram
 141end Foundation
 142end IndisputableMonolith

depends on (12)

Lean names referenced from this declaration's body.