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

locality_forces_additive_composition

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)

  72theorem locality_forces_additive_composition
  73    (L : UniformScaleLadder)
  74    (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
  75    L.ratio ^ 2 = L.ratio + 1 := by

proof body

Tactic-mode proof.

  76  have h0 : L.levels 0 ≠ 0 := ne_of_gt (L.levels_pos 0)
  77  have h1 : L.levels 1 = L.ratio * L.levels 0 := L.uniform_scaling 0
  78  have h2 : L.levels 2 = L.ratio * L.levels 1 := L.uniform_scaling 1
  79  have h_sq : L.levels 2 = L.ratio ^ 2 * L.levels 0 := by
  80    rw [h2, h1]; ring
  81  have h_rhs : L.levels 2 = (L.ratio + 1) * L.levels 0 := by
  82    rw [additive_closure, h1]; ring
  83  have h_mul : (L.ratio ^ 2 - (L.ratio + 1)) * L.levels 0 = 0 := by
  84    calc
  85      (L.ratio ^ 2 - (L.ratio + 1)) * L.levels 0
  86          = L.ratio ^ 2 * L.levels 0 - (L.ratio + 1) * L.levels 0 := by ring
  87      _ = L.levels 2 - L.levels 2 := by rw [← h_sq, h_rhs]
  88      _ = 0 := by ring
  89  rcases mul_eq_zero.mp h_mul with hzero | hsize
  90  · exact sub_eq_zero.mp hzero
  91  · exact (h0 hsize).elim
  92
  93/-- **Bridge B1 (unconditional)**: from a zero-parameter scale ladder
  94with additive composition, the scale ratio is forced to `φ`. -/

used by (3)

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

depends on (11)

Lean names referenced from this declaration's body.