theorem proved term proof

`deltaCP_pmns_leading_order_zero`

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

formal statement (Lean)

 286theorem deltaCP_pmns_leading_order_zero :
 287    (0 : ℝ) = (2 : ℕ) * Real.pi / 4 - (2 : ℕ) * Real.pi / 4 := by ring

proof body

Term-mode proof.

 288
 289/-- The torsion correction to δ_CP(PMNS):
 290    Δτ₂₃/Δτ₁₂ × (π/4) = 6/11 × π/4 ≈ 0.428 rad.
 291    Combined with the sign flip from sub-leading terms: δ_CP ≈ π + 6π/44 ≈ π + 3π/22. -/

depends on (4)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
sub in IndisputableMonolith.Numerics.Interval.Basic decl_use
sub in IndisputableMonolith.RecogSpec.Core decl_use