`programSpec_injective`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalProgram
domain: Foundation
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalProgram on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  45  pipeline := pipelineSpec c
  46  ready := empiricallyReady_all c
  47
  48theorem programSpec_injective : Function.Injective programSpec := by
  49  intro a b h
  50  exact congrArg ProgramSpec.combination h
  51
  52/-- First-pass empirical program in execution order. -/
  53def firstPassProgram : List ProgramSpec :=
  54  firstPassSchedule.map programSpec
  55
  56theorem firstPassProgram_length :
  57    firstPassProgram.length = 5 := by
  58  unfold firstPassProgram
  59  rw [List.length_map, firstPassSchedule_length]
  60
  61theorem firstPassProgram_nodup :
  62    firstPassProgram.Nodup := by
  63  unfold firstPassProgram
  64  exact List.Nodup.map programSpec_injective firstPassSchedule_nodup
  65
  66/-- The first-pass program contains exactly the high-or-immediate tests. -/
  67theorem firstPassProgram_exact_top_priority (c : CombinationID) :
  68    c ∈ firstPassSchedule ↔ isHighOrImmediate c :=
  69  firstPassSchedule_mem_iff_high_or_immediate c
  70
  71theorem scheduled_program_ready
  72    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  73    (programSpec c).ready = empiricallyReady_all c :=
  74  rfl
  75
  76theorem scheduled_program_pipeline
  77    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  78    (programSpec c).pipeline = pipelineSpec c :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.