theorem proved term proof

`Az_eq`

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

formal statement (Lean)

  62theorem Az_eq : Az = 1 := by

Term-mode proof.

  63  simp [Az, active_edges_per_tick]
  64
  65/-! ## Alternative derivation formulas -/
  66
  67/-- Alternative formula for B_pow. -/

Lean names referenced from this declaration's body.

active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
B_pow in IndisputableMonolith.Masses.Anchor decl_use
Az in IndisputableMonolith.Masses.AnchorDerivation decl_use