def definition def or abbrev

`correction_D_half`

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

formal statement (Lean)

  65noncomputable def correction_D_half (d : ℕ) : ℝ := (d : ℝ) / 2

Definition body.

  66
  67/-- Candidate 2: F/4 = (2D)/4 = D/2 (algebraically equivalent!) -/

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

D_half_admissible in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
D_half_at_3 in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
F_quarter_admissible in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
F_quarter_eq_D_half in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
F_quarter_not_alternative in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
tau_correction_unique_admissible in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use

Lean names referenced from this declaration's body.

Candidate in IndisputableMonolith.Foundation.Atomicity decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use