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

structural_dominance

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)

 242theorem structural_dominance {f : Fermion} (pr : PerturbativeResidue f)
 243    (hlaw : geometricResidue f = coshEnhancement pr.value * pr.value) :
 244    pr.value < geometricResidue f := by

proof body

Term-mode proof.

 245  rw [hlaw]
 246  have hS := enhancement_gt_one pr.value (ne_of_gt pr.positive)
 247  have hv := pr.positive
 248  nlinarith
 249
 250/-! ## §7. The Coupling Certificate -/
 251
 252/-- The coupling law certificate: packages the full bridge. -/

depends on (10)

Lean names referenced from this declaration's body.