deliverable_count
plain-language theorem explainer
The theorem establishes that the inductive type of empirical deliverables for the Option A plan enumerates exactly nine artifacts. Analysts validating the Recognition Science empirical pipeline would cite this cardinality to confirm the scheduled output set is complete. The proof is a one-line decide tactic that computes the finite type cardinality directly from the enumerated constructors.
Claim. The type of empirical deliverables has cardinality nine: $ |Deliverable| = 9 $.
background
The module specifies concrete artifacts expected from the Option A empirical action plan and converts the first-pass schedule into an auditable collection of outputs. Deliverable is an inductive type with nine constructors: oncologyFactorModelNotebook, memoryCollapseNotebook, attentionPlateauPlot, regulatoryCeilingTable, planetPhiRatioTable, cognitiveDecoderBenchmark, responseCoefficientPanel, quantumAddressingBenchmark, and eriksonReverseCohortTable. Upstream definitions of the active edge count A include the phi-power balance identity at D = 3: φ^(A − gap) · φ^gap = φ, equivalently φ^(−44) · φ^45 = φ.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card Deliverable = 9. The tactic succeeds by reflection on the finite inductive type whose constructors are explicitly listed.
why it matters
This result supplies the nine_deliverables field inside empiricalDeliverablesCert, which certifies the full deliverable set for the Option A plan. It anchors the empirical validation layer of the Recognition Science foundation by providing an auditable count of required artifacts without axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.