pith. machine review for the scientific record. sign in
theorem proved tactic proof

inevitability

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 172theorem inevitability (F : AlternativeFramework)
 173    (h_zero : zero_parameter F)
 174    (h_obs : F.derives_observables) :
 175    (F.cost = RS_framework.cost ∧ F.selection = RS_framework.selection) ∨
 176    (∃ g ∈ all_gates, violates_gate F g) := by

proof body

Tactic-mode proof.

 177  by_cases h_rs : (F.cost = RS_framework.cost ∧ F.selection = RS_framework.selection)
 178  · left; exact h_rs
 179  · right
 180    -- h_rs : ¬(F.cost = RS_framework.cost ∧ F.selection = RS_framework.selection)
 181    -- Split on whether costs match
 182    by_cases h_cost : F.cost = RS_framework.cost
 183    · -- Costs match, so selection must differ
 184      have h_sel : F.selection ≠ RS_framework.selection := by
 185        intro h_sel_eq
 186        exact h_rs ⟨h_cost, h_sel_eq⟩
 187      use gate_selection_rule
 188      constructor
 189      · simp [all_gates]
 190      · unfold violates_gate
 191        simp [gate_selection_rule, h_sel]
 192    · -- Costs differ
 193      use gate_cost_uniqueness
 194      constructor
 195      · simp [all_gates]
 196      · unfold violates_gate
 197        simp [gate_cost_uniqueness, h_cost]
 198
 199/-! ## The Choke Point Analysis -/
 200
 201/-- A choke point is a place where alternatives can hide unless proven closed. -/

used by (20)

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

depends on (21)

Lean names referenced from this declaration's body.