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

quartic_coupling_from_normalization

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)

 220theorem quartic_coupling_from_normalization
 221    (Λ v m_H : ℝ) (hv : 0 < v) (hΛ : NormalizationHypothesis Λ v m_H) :
 222    4 * quartic_coefficient_canonical Λ v = m_H ^ 2 / (6 * v ^ 2) := by

proof body

Tactic-mode proof.

 223  unfold quartic_coefficient_canonical
 224  unfold NormalizationHypothesis at hΛ
 225  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hv)
 226  have hv4 : v ^ 4 ≠ 0 := pow_ne_zero 4 (ne_of_gt hv)
 227  have hv4_eq : (v : ℝ) ^ 4 = v ^ 2 * v ^ 2 := by ring
 228  rw [hΛ, hv4_eq]
 229  field_simp
 230  ring
 231
 232/-! ## §4. Master Bridge Certificate -/
 233
 234/-- Master certificate for the cost-geometry → scalar-EFT map.
 235
 236    Tags: each clause is `THEOREM` except where marked `CONDITIONAL_THEOREM`;
 237    those clauses depend on `NormalizationHypothesis Λ v m_H`. -/

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.