theorem proved term proof

`orbitLevels_two`

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

formal statement (Lean)

  79@[simp] theorem orbitLevels_two : orbitLevels 2 = 1 := by

Term-mode proof.

  80  simp [orbitLevels, boolFramework, baseState]
  81
  82/-- The counterexample orbit does not satisfy ratio self-similarity. -/

Lean names referenced from this declaration's body.

baseState in IndisputableMonolith.Foundation.HierarchyRealizationObstruction decl_use
boolFramework in IndisputableMonolith.Foundation.HierarchyRealizationObstruction decl_use
orbitLevels in IndisputableMonolith.Foundation.HierarchyRealizationObstruction decl_use
self in IndisputableMonolith.RecogSpec.Core decl_use