def definition def or abbrev

`ckm_cp_phase`

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

formal statement (Lean)

 269noncomputable def ckm_cp_phase : ℝ := Real.pi / 2

proof body

Definition body.

 270
 271/-- **Geometric Origin of Jarlskog Invariant**
 272    The Jarlskog invariant J_CP is the geometric area of the unitarity triangle,
 273    forced by the cube topology and the fine-structure leakage.
 274    J = s12 s23 s13 c12 c23 c13 sin δ
 275    Approximated geometrically as:
 276    J ≈ (1/24) * (α/2) * (φ⁻³) * sin(π/2) -/

used by (4)

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

jarlskog_witness_pos in IndisputableMonolith.Physics.CKM decl_use
jarlskog_match in IndisputableMonolith.Physics.MixingDerivation decl_use
jarlskog_pos in IndisputableMonolith.Physics.MixingDerivation decl_use
jarlskog_pred in IndisputableMonolith.Physics.MixingDerivation decl_use

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use