`baseState`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.HierarchyRealizationObstruction
domain: Foundation
line: 68 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.HierarchyRealizationObstruction on GitHub at line 68.

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

  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
  74  simp [orbitLevels, boolFramework, baseState]
  75
  76@[simp] theorem orbitLevels_one : orbitLevels 1 = 2 := by
  77  simp [orbitLevels, boolFramework, baseState]
  78
  79@[simp] theorem orbitLevels_two : orbitLevels 2 = 1 := by
  80  simp [orbitLevels, boolFramework, baseState]
  81
  82/-- The counterexample orbit does not satisfy ratio self-similarity. -/
  83theorem orbit_not_ratio_self_similar :
  84    ¬ (∀ k,
  85      orbitLevels (k + 2) / orbitLevels (k + 1) =
  86        orbitLevels (k + 1) / orbitLevels k) := by
  87  intro h
  88  have h0 := h 0
  89  simp [orbitLevels, boolFramework, baseState] at h0
  90  norm_num at h0
  91
  92/-- The counterexample orbit does not satisfy additive posting. -/
  93theorem orbit_not_additive_posting :
  94    ¬ (orbitLevels 2 = orbitLevels 1 + orbitLevels 0) := by
  95  simp [orbitLevels, boolFramework, baseState]
  96
  97/-- Therefore `ClosedObservableFramework` alone cannot force
  98`ratio_self_similar`. -/

papers checked against this theorem

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