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

power_ethics_same_axis

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)

  62theorem power_ethics_same_axis (x : ℝ) (hx : 0 < x) (hne : x ≠ 1) :
  63    coherenceLevel x hx < coherenceLevel 1 one_pos := by

proof body

Term-mode proof.

  64  rw [max_coherence_at_balance]
  65  unfold coherenceLevel
  66  have hJ : 0 < Jcost x := Jcost_pos_of_ne_one x hx hne
  67  rw [div_lt_one (by linarith [Jcost_nonneg hx])]
  68  linarith
  69
  70/-- Weaponization requires σ > 0, which reduces coherence below maximum. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.