Measurement Window Neutrality Gap Weight Pos

The positive gap weight

In the Recognition Science framework, a ledger is a discrete record of events, and a window is a fixed-size slice of that record. An eight-tick window is neutral when its signed sum is zero: treat each event as plus one or minus one, add them across the eight positions, and require the total to vanish. The framework's library, a machine-checked collection of formal theorems, proves that any such neutral window can be assigned a consistent potential, a number attached to each position that explains the differences between the window's entries.

From that neutrality condition, the framework derives a specific number called the gap weight, denoted w₈. The value is not chosen freely; it is uniquely determined by the eight-tick minimality condition that comes from the framework's scaling theorem. The declaration gap_weight_pos proves that this number is positive, that is, greater than zero. The proof is a direct consequence of the closed-form definition of w₈, which the library states explicitly.

The positivity is not a numerical accident. It is a theorem in the machine-checked library, meaning it follows from the framework's axioms and definitions with no unproved assumptions. The declaration does not, however, claim anything about the magnitude of w₈, nor does it connect the gap weight to any measured physical constant. It establishes only the sign, and that sign is a formal consequence of the definitions, not an empirical observation.

What the declaration does not claim is as important as what it proves. It does not say that the gap weight equals any particular number, such as the fine-structure constant or its inverse. It does not say that the gap weight is derived from experiment. It does not say that the positivity holds for all possible ledgers; it holds for the specific w₈ defined in the framework's constants module. The theorem is a precise, narrow statement: the defined quantity is positive.

/-- A window is neutral if its signed sum is zero -/
def isNeutralWindow (w : Pattern 8) : Prop :=
  ∑ i : Fin 8, (if w i then (1 : ℤ) else (-1 : ℤ)) = 0

/-- Eight-tick neutral window implies existence of potential -/
theorem eight_tick_neutral_implies_exact (w : Pattern 8)
  (hneutral : isNeutralWindow w) :
  ∃ φ : Pattern 8 → ℤ,
    ∀ i j : Fin 8,
      (if w j then 1 else -1) - (if w i then 1 else -1) =
      φ (fun _ => w j) - φ (fun _ => w i) := by
  -- For a simpler proof, we construct φ as the cumulative sum up to each position
  -- Define φ(pattern) to be the value at position 0 of that pattern
  -- Then differences are just the single-position values
  let φ : Pattern 8 → ℤ := fun p => if p 0 then 1 else -1
  use φ
  intro i j
  -- The key insight: we're mapping patterns to integers based on their value at position 0
  -- The difference of pattern values equals the potential difference
  simp [φ]

/-- 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

What this page does not claim

The gap weight equals any specific measured constant, such as the fine-structure constant. The positivity is an empirical measurement rather than a formal theorem. The declaration establishes the magnitude or any other property of w₈ beyond its sign.

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: