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

gap_balance

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)

 109theorem gap_balance :
 110    phi ^ (A - ↑(integrationGap D)) * phi ^ (↑(integrationGap D) : ℤ) = phi := by

proof body

Tactic-mode proof.

 111  have hg : (↑(integrationGap D) : ℤ) = 45 := by exact_mod_cast integrationGap_at_D3
 112  rw [hg, show A = (1 : ℤ) from rfl, ← zpow_add₀ (ne_of_gt phi_pos)]
 113  have : (1 : ℤ) - 45 + 45 = 1 := by norm_num
 114  rw [this, zpow_one]
 115
 116end
 117
 118/-! ## Master certificate -/
 119

depends on (6)

Lean names referenced from this declaration's body.