`gap_weight_unique`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.WindowNeutrality
domain: Measurement
line: 47 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.WindowNeutrality on GitHub at line 47.

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

  44
  45/-- The gap weight w₈ is uniquely determined by T6 eight-tick minimality.
  46    The value is defined as a closed form in `Constants.GapWeight.w8_from_eight_tick`. -/
  47theorem gap_weight_unique :
  48  ∃! w : ℝ, w = w8_from_eight_tick := by
  49  use w8_from_eight_tick
  50  constructor
  51  · rfl
  52  · intro y hy; exact hy
  53
  54/-- The gap weight is positive (derived from the closed form). -/
  55theorem gap_weight_pos : 0 < w8_from_eight_tick := w8_pos
  56
  57end Measurement
  58end IndisputableMonolith

papers checked against this theorem

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