Measurement Window Neutrality Gap Weight Unique

The unique gap weight

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is a single entry in that record. The framework studies how such records must behave if they are to be consistent. One of its objects is the eight-tick window: a sequence of eight entries, each marked as a positive or negative recognition. A window is called neutral when its signed sum is zero, meaning it contains exactly four positive and four negative entries.

The declaration gap_weight_unique proves that a particular real number, called the gap weight and written w₈, is uniquely determined by the requirement that eight-tick windows be neutral. The proof shows there is exactly one such number, and that it is positive. This is a formal theorem in the framework's machine-checked library of formal theorems, not a conjecture or a numerical approximation.

The gap weight appears in the framework's derivation of the inverse fine-structure constant α⁻¹. The neutrality of eight-tick windows fixes this weight, which then enters the calculation of α⁻¹. The uniqueness result is therefore a link in a chain: it says that the structure of the measurement window forces a specific number, rather than leaving it free.

What the declaration does not claim is just as important. It does not say that the gap weight equals any particular numerical value; it only proves existence and uniqueness of a positive real number. It does not claim that this weight, by itself, produces the measured value of α⁻¹; the full derivation involves additional steps and identifications. And it does not claim that the eight-tick window is the only possible measurement structure; it only analyzes the consequences of choosing this one.

/-- The gap weight w₈ is uniquely determined by T6 eight-tick minimality.
    The value is defined as a closed form in `Constants.GapWeight.w8_from_eight_tick`. -/
theorem gap_weight_unique :
  ∃! w : ℝ, w = w8_from_eight_tick := by
  use w8_from_eight_tick
  constructor
  · rfl
  · intro y hy; exact hy

/-- The gap weight is positive (derived from the closed form). -/
theorem gap_weight_pos : 0 < w8_from_eight_tick := w8_pos

/-- The gap weight w₈ is uniquely determined by T6 eight-tick minimality.
    The value is defined as a closed form in `Constants.GapWeight.w8_from_eight_tick`. -/
theorem gap_weight_unique :
  ∃! w : ℝ, w = w8_from_eight_tick := by
  use w8_from_eight_tick
  constructor
  · rfl
  · intro y hy; exact hy

What this page does not claim

The gap weight is not assigned a specific numerical value by this declaration. The uniqueness of w₈ does not by itself produce the measured value of α⁻¹. The eight-tick window is not claimed to be the only possible measurement structure in the framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/WindowNeutrality.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: