def definition def or abbrev

`TBM_correction_theta12`

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

formal statement (Lean)

 139noncomputable def TBM_correction_theta12 : ℝ := 1/3 - sin2_theta12_observed

proof body

Definition body.

 140
 141/-- The 8-tick connection:
 142
 143    With 8 phases and 3 generations, we have 24 degrees of freedom.
 144    The mixing angles partition these into mass and flavor bases.
 145
 146    The specific angles may emerge from minimizing J-cost
 147    when transforming between bases. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
sin2_theta12_observed in IndisputableMonolith.StandardModel.PMNSMatrix decl_use