`recordProgressionCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Sport.RecordProgressionFit
domain: Sport
line: 79 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Sport.RecordProgressionFit on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  76  strictly_decreasing : ∀ N, gapAt (N + 1) < gapAt N
  77
  78/-- Athletic-record-progression fit certificate. -/
  79def recordProgressionCert : RecordProgressionCert where
  80  gap_pos := gapAt_pos'
  81  one_step_ratio := gapAt_succ_ratio
  82  consecutive_ratio := consecutive_gap_ratio
  83  strictly_decreasing := gapAt_strictly_decreasing
  84
  85end
  86end RecordProgressionFit
  87end Sport
  88end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.