theorem proved term proof

`deltaCP_pmns_in_third_quadrant`

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

formal statement (Lean)

 296theorem deltaCP_pmns_in_third_quadrant :
 297    Real.pi < deltaCP_pmns_torsion_correction ∧
 298    deltaCP_pmns_torsion_correction < 3 * Real.pi / 2 := by

proof body

Term-mode proof.

 299  unfold deltaCP_pmns_torsion_correction
 300  constructor
 301  · linarith [Real.pi_pos]
 302  · linarith [Real.pi_pos]
 303
 304/-- δ_CP(PMNS) ∈ (π, 2π) — consistent with the observed ≈ 197° = 1.094π. -/

used by (1)

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

deltaCP_pmns_range in IndisputableMonolith.StandardModel.PMNSMatrix decl_use

depends on (2)

Lean names referenced from this declaration's body.

consistent in IndisputableMonolith.Complexity.SAT.Backprop decl_use
deltaCP_pmns_torsion_correction in IndisputableMonolith.StandardModel.PMNSMatrix decl_use