def definition def or abbrev

`quarter`

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

formal statement (Lean)

  28@[simp] def quarter (k : ℤ) : Rung := (k : ℚ) / 4

proof body

Definition body.

  29
  30/-- The half‑ladder embedding: `k ↦ k/2`. -/

used by (27)

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

per_turn_at_kappa_one in IndisputableMonolith.Flight.TeslaTurbine decl_use
C_xi_pos in IndisputableMonolith.Gravity.GravityParameters decl_use
down_generation_ordering in IndisputableMonolith.Masses.SectorDependentTorsion decl_use
pi_over_4_fundamental in IndisputableMonolith.Mathematics.Pi decl_use
phi_in_phiIntervalTight in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
phi_neg58_lt in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
phi_quarter_bounds in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
phi_quarter_lt in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
nu1_spacing_eq in IndisputableMonolith.Physics.NeutrinoSector decl_use
nu_spacing_eq in IndisputableMonolith.Physics.NeutrinoSector decl_use
predicted_mass_eV_legacy in IndisputableMonolith.Physics.NeutrinoSector decl_use
res_nu2 in IndisputableMonolith.Physics.NeutrinoSector decl_use
SMDerivation in IndisputableMonolith.Physics.ParticleSummary decl_use
Convention in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
conventions_differ_bottom in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
core_dependent_claims in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
core_down_rungs in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
core_uses_integer_rungs in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
hypothesis_positions in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
QuarkQuarterLadderPositions in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
quarter_ladder_is_hypothesis in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
quarter_step in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
quarter_to_real in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
Resolution in IndisputableMonolith.Physics.QuarkCoordinateReconciliation decl_use
residues_match_steps in IndisputableMonolith.Physics.QuarkMasses decl_use
ofInt in IndisputableMonolith.Support.RungFractions decl_use
quarter_eq in IndisputableMonolith.Support.RungFractions decl_use

depends on (4)

Lean names referenced from this declaration's body.

half in IndisputableMonolith.QFT.SpinStatistics decl_use
half in IndisputableMonolith.RecogSpec.Core decl_use
half in IndisputableMonolith.Support.RungFractions decl_use
Rung in IndisputableMonolith.Support.RungFractions decl_use