rung — Recognition explainer

formal statement (Lean)

  40def rung : ℕ := 1

proof body

Definition body.

  41
  42end Fermion
  43end RSBridge

used by (40)

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

hearingLossPenalty_zero in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
GeometricStrain in IndisputableMonolith.Applied.CoherenceTechnology decl_use
E_base_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
E_PBM_bounds in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
eV_to_J_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
settlementLevelCount_eq in IndisputableMonolith.Archaeology.UrbanDensityFromPhiLadder decl_use
referenceTime in IndisputableMonolith.Astrophysics.CoronalLyapunovTime decl_use
BIT_carrier_period_band in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
fast_radio_burst_one_statement in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
FRB_amplification_factor_eq in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
FRB_period_geometric in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
FRB_period_strict_increasing in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
ml_nucleosynthesis_eq_phi in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
referenceExponent in IndisputableMonolith.Astrophysics.PICSimulationLyapunov decl_use
AgreesAtHalfRung in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
planetaryFormationCert in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
r_orbit_adjacent_ratio in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
r_orbit_adjacent_ratio_band in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
r_orbit_closed in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
r_orbit_gap_skip_band in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
two_rung_gap_eq_phi_squared in IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost decl_use
bimodal_ratio_gt_thirty in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
bimodal_ratio_lt_phi_nine in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
gap_size_pos in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
normal_median_rung in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
pulsar_period_one_statement in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
recycling_rung_shift_eq in IndisputableMonolith.Astrophysics.PulsarPeriodFromRung decl_use
E_coh in IndisputableMonolith.Chemistry.ActivationEnergy decl_use
different_rungs_different_barriers in IndisputableMonolith.Chemistry.EnzymeCatalysis decl_use
rate_enhancement in IndisputableMonolith.Chemistry.EnzymeCatalysis decl_use

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
RSBridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use