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

orbit_not_ratio_self_similar

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)

  83theorem orbit_not_ratio_self_similar :
  84    ¬ (∀ k,
  85      orbitLevels (k + 2) / orbitLevels (k + 1) =
  86        orbitLevels (k + 1) / orbitLevels k) := by

proof body

Term-mode proof.

  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. -/

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.