boolFramework

formal source

  40
  41/-- A finite closed-observable framework whose orbit alternates between
  42observable values `1` and `2`. -/
  43def boolFramework : ClosedObservableFramework where
  44  S := Bool
  45  T := not
  46  r := fun b => if b then 2 else 1
  47  r_pos := by
  48    intro b
  49    cases b <;> norm_num
  50  nontrivial := by
  51    refine ⟨false, true, ?_⟩
  52    norm_num
  53  S_countable := by
  54    refine ⟨fun n => if n % 2 = 0 then false else true, ?_⟩
  55    intro b
  56    cases b
  57    · refine ⟨0, ?_⟩
  58      simp
  59    · refine ⟨1, ?_⟩
  60      simp
  61  no_continuous_moduli := no_injective_real_to_bool
  62  charge := fun _ => 0
  63  charge_conserved := by
  64    intro s
  65    rfl
  66
  67/-- The base state used for the obstruction. -/
  68def baseState : boolFramework.S := false
  69
  70/-- The orbit-defined levels of the counterexample framework. -/
  71def orbitLevels (k : ℕ) : ℝ := boolFramework.r (boolFramework.T^[k] baseState)
  72
  73@[simp] theorem orbitLevels_zero : orbitLevels 0 = 1 := by