abbrev definition def or abbrev

`Rung`

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

formal statement (Lean)

  22abbrev Rung := ℚ

proof body

Definition body.

  23
  24/-- Embed an integer rung into a rational rung. -/

used by (40)

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

phi_energy_rung_step in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
phi_energy_rung_zero in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
atmospheric_layering_one_statement in IndisputableMonolith.Climate.AtmosphericLayeringFromPhiLadder decl_use
animal_z_complexity_one_statement in IndisputableMonolith.Cognition.AnimalZComplexityBound decl_use
z_rung_pos in IndisputableMonolith.Cognition.AnimalZComplexityBound decl_use
worldClassRung in IndisputableMonolith.Education.MasteryThresholdFromGap45 decl_use
closure_populates_next in IndisputableMonolith.Foundation.StillnessGenerative decl_use
r_ref_exact_gt_r in IndisputableMonolith.Gravity.RunningG decl_use
r_down in IndisputableMonolith.Masses.Anchor decl_use
r_lepton_values in IndisputableMonolith.Masses.Anchor decl_use
r_up in IndisputableMonolith.Masses.Anchor decl_use
tau_values in IndisputableMonolith.Masses.Anchor decl_use
minimal_complete_coefficients in IndisputableMonolith.Masses.BaselineDerivation decl_use
cos2_theta_positive in IndisputableMonolith.Masses.ElectroweakMasses decl_use
m_t_exp in IndisputableMonolith.Masses.QuarkVerification decl_use
quark_mass_positive in IndisputableMonolith.Masses.QuarkVerification decl_use
genOf_surjective in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
match_rsbridge_rung in IndisputableMonolith.Masses.RungConstructor.Proofs decl_use
tauon_rung_minus_electron_rung in IndisputableMonolith.Masses.SMVerification decl_use
m_tau_exp in IndisputableMonolith.Masses.Verification decl_use
pitchJND_jcost_pos in IndisputableMonolith.MusicTheory.PitchPerceptionFromPhiLadder decl_use
pitchJND_one in IndisputableMonolith.MusicTheory.PitchPerceptionFromPhiLadder decl_use
pitch_perception_one_statement in IndisputableMonolith.MusicTheory.PitchPerceptionFromPhiLadder decl_use
phiRungWavenumber in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
phiRungWavenumber_succ in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
pmns_prob in IndisputableMonolith.Physics.MixingDerivation decl_use
nu1_spacing in IndisputableMonolith.Physics.NeutrinoSector decl_use
nu_phase_offset in IndisputableMonolith.Physics.NeutrinoSector decl_use
nu_spacing in IndisputableMonolith.Physics.NeutrinoSector decl_use
predicted_mass_eV_frac in IndisputableMonolith.Physics.NeutrinoSector decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use