theorem proved term proof

`down_Z_is_24`

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

formal statement (Lean)

  51theorem down_Z_is_24 : ZOf d = 24 := by native_decide

proof body

Term-mode proof.

  52
  53/-! ## Lepton Certificates
  54    Leptons fit the integer rung model well.
  55    Audit data (delta shifted by +34.66):
  56    - e:   13.954
  57    - μ:   14.034
  58    - τ:   13.899
  59    Theoretical target: F(1332) ≈ 13.954
  60-/
  61

depends on (14)

Lean names referenced from this declaration's body.

model in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
rung in IndisputableMonolith.Compat.Constants decl_use
delta in IndisputableMonolith.Cost.Ndim.Connections decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
Lepton in IndisputableMonolith.Physics.AnomalousMoments decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.RSBridge.Anchor decl_use