def definition def or abbrev

`fine_structure_leakage`

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

formal statement (Lean)

  34noncomputable def fine_structure_leakage : ℝ := Constants.alpha / 2

proof body

Definition body.

  35
  36/-- The 3-generation torsion overlap on the cubic ledger.
  37    This corresponds to the delocalization of the first generation
  38    across the three spatial dimensions. -/

used by (12)

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

jarlskog_witness_pos in IndisputableMonolith.Physics.CKM decl_use
CKMElementScoreCardCert in IndisputableMonolith.Physics.CKMElementScoreCard decl_use
row_vub_eq_leakage in IndisputableMonolith.Physics.CKMElementScoreCard decl_use
V_ub_err in IndisputableMonolith.Physics.CKMGeometry decl_use
V_ub_match in IndisputableMonolith.Physics.CKMGeometry decl_use
V_ub_pred in IndisputableMonolith.Physics.CKMGeometry 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
MixingCert in IndisputableMonolith.Physics.MixingDerivation decl_use
vcb_derived in IndisputableMonolith.Physics.MixingDerivation decl_use
vub_derived in IndisputableMonolith.Physics.MixingDerivation decl_use

depends on (8)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
alpha in IndisputableMonolith.Constants.Alpha decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
overlap in IndisputableMonolith.YM.Dobrushin decl_use