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

predict_mass_pos

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)

  44theorem predict_mass_pos (s : Sector) (r : ℤ) (Z_val : ℤ) :
  45    predict_mass s r Z_val > 0 := by

proof body

Term-mode proof.

  46  unfold predict_mass
  47  apply mul_pos
  48  · -- yardstick is positive
  49    unfold yardstick Anchor.E_coh
  50    apply mul_pos
  51    · apply mul_pos
  52      · exact zpow_pos (by norm_num) (B_pow s)
  53      · exact zpow_pos phi_pos (-5 : ℤ)
  54    · exact zpow_pos phi_pos (r0 s)
  55  · -- phi^... is positive
  56    exact Real.rpow_pos_of_pos phi_pos _
  57
  58/-! ## Derived Properties -/
  59
  60/-- The mass law exhibits φ-scaling: increasing rung by 1 scales mass by φ. -/

used by (13)

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

depends on (19)

Lean names referenced from this declaration's body.