lemma proved term proof

`E_passive_exact`

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

formal statement (Lean)

 165lemma E_passive_exact : (E_passive : ℝ) = 11 := by

Term-mode proof.

 166  have h : (E_passive : ℕ) = 11 := rfl
 167  simp only [h, Nat.cast_ofNat]
 168
 169/-- Cube faces = 6 (exact). -/

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

lepton_ladder_forced_from_T9 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
lepton_ladder_forced_from_T9_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
step_e_mu_bounds in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
step_e_mu_bounds_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
E_passive_exact in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use
lepton_ladder_forced_from_T9 in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use
step_e_mu_bounds in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use

Lean names referenced from this declaration's body.

E_passive in IndisputableMonolith.Masses.Anchor decl_use
E_passive in IndisputableMonolith.Physics.MassTopology decl_use
E_passive_exact in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use