theorem proved term proof

`realized_uniform_ratios`

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

formal statement (Lean)

  94theorem realized_uniform_ratios (F : ClosedObservableFramework)
  95    (H : RealizedHierarchy F) :
  96    ∀ j k, H.levels (j + 1) / H.levels j = H.levels (k + 1) / H.levels k := by

proof body

Term-mode proof.

  97  intro j k
  98  rw [realized_ratio_eq_base F H j, realized_ratio_eq_base F H k]
  99
 100/-- Construct a `UniformScaleLadder` from a realized hierarchy. -/

used by (2)

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

NontrivialMultilevelComposition in IndisputableMonolith.Foundation.HierarchyForcing decl_use
realized_to_ladder in IndisputableMonolith.Foundation.HierarchyRealization decl_use

depends on (10)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
ClosedObservableFramework in IndisputableMonolith.Foundation.ClosedObservableFramework decl_use
UniformScaleLadder in IndisputableMonolith.Foundation.HierarchyEmergence decl_use
RealizedHierarchy in IndisputableMonolith.Foundation.HierarchyRealization decl_use
realized_ratio_eq_base in IndisputableMonolith.Foundation.HierarchyRealization decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use