abbrev definition def or abbrev

`E_total`

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

formal statement (Lean)

  58abbrev E_total : ℕ := cube_edges D

proof body

Definition body.

  59
  60/-- Active edges per tick: 1 -/

used by (28)

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

B_pow in IndisputableMonolith.Masses.Anchor decl_use
B_pow_DownQuark_eq in IndisputableMonolith.Masses.Anchor decl_use
r0 in IndisputableMonolith.Masses.Anchor decl_use
r0_DownQuark_eq in IndisputableMonolith.Masses.Anchor decl_use
B_pow_eq_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
r0_eq_alt in IndisputableMonolith.Masses.AnchorDerivation decl_use
base_shift_denominator_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
base_shift_denominator_forced_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
base_shift_denominator_scale_forced_no_hc_pos in IndisputableMonolith.Masses.JCostPerturbation decl_use
base_shift_kn_forced_under_passive_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
base_shift_kn_forced_under_passive_bound_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
base_shift_numerator_offset_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
base_shift_weight_split_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_denominator_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_denominator_forced_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_denominator_scale_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_denominator_scale_forced_no_hc_pos in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_kn_forced_under_passive_bound in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_kn_forced_under_passive_bound_no_hk in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_numerator_offset_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
ledger_fraction_weight_split_forced in IndisputableMonolith.Masses.JCostPerturbation decl_use
mass_topology_counts in IndisputableMonolith.Masses.JCostPerturbation decl_use
lepton_sector_is_derived in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
ledger_fraction_exact in IndisputableMonolith.Physics.ElectronMass.Necessity decl_use
radiative_correction_bounds in IndisputableMonolith.Physics.ElectronMass.Necessity decl_use
correction_order_3 in IndisputableMonolith.Physics.MassTopology decl_use
E_total in IndisputableMonolith.Physics.MassTopology decl_use
ledger_fraction in IndisputableMonolith.Physics.MassTopology decl_use

depends on (4)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
cube_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
E_total in IndisputableMonolith.Physics.MassTopology decl_use