empiricalProgramCert
plain-language theorem explainer
The definition constructs the top-level certificate EmpiricalProgramCert for the first-pass empirical program in Option A by bundling proofs of program injectivity, list length five, absence of duplicates, readiness, completeness, and priority conditions. A researcher verifying the empirical readiness of Recognition Science's Option A would reference this certificate as the single object confirming metadata integrity. The construction is a direct structure literal delegating each requirement to a dedicated upstream lemma.
Claim. Let EmpiricalProgramCert be the structure requiring that programSpec is injective, firstPassProgram has length 5 and is nodup, FirstPassReady holds, FirstPassProgramComplete holds, every c in firstPassSchedule satisfies (programSpec c).ready = empiricallyReady_all c together with the scheduled pipeline condition, action classes are nodup, deliverable classes are nodup, pipeline records are nodup, and firstPassSchedule contains exactly the high-or-immediate tests. Then empiricalProgramCert is the explicit witness obtained by substituting the corresponding lemmas for each field.
background
EmpiricalProgramCert is the structure defined in this module that packages all metadata constraints for the first-pass program attached to Option A. Its fields include program_injective requiring Function.Injective programSpec, first_pass_length requiring firstPassProgram.length = 5, first_pass_nodup requiring firstPassProgram.Nodup, first_pass_ready : FirstPassReady, first_pass_complete : FirstPassProgramComplete, and further conditions on scheduled readiness, pipelines, and uniqueness of actions, deliverables, and pipelines. The module doc states that this file proves the assembled first-pass program is complete and collision-free at the metadata layer, with zero sorry or axiom.
proof idea
The definition is a record literal that directly assigns each field of the EmpiricalProgramCert structure to the corresponding theorem or lemma already established in the module: program_injective to programSpec_injective, first_pass_length to firstPassProgram_length, and similarly for the remaining nine fields using firstPassProgram_nodup, FirstPassReady, firstPassProgramComplete, scheduled_program_ready, scheduled_program_pipeline, firstPassProgram_actions_nodup, firstPassProgram_deliverables_nodup, firstPassProgram_pipelines_nodup, and firstPassProgram_exact_top_priority.
why it matters
This definition supplies the single assembled certificate that the first-pass empirical program for Option A satisfies all required properties without collisions or incompleteness. It closes the empirical program construction in the Foundation layer. The module establishes that the program is collision-free at the metadata layer, aligning with the Recognition Science goal of deriving empirical readiness from the forcing chain without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.