IndisputableMonolith.Measurement.WindowNeutrality
The WindowNeutrality module defines the predicate for neutral windows where the signed sum over an eight-tick interval equals zero. Periodic table constructions cite it to locate noble-gas closures in the zero-parameter chemistry scaffold. The module consists of a core definition plus direct lemmas establishing exactness, uniqueness, and positivity from the signed-sum condition.
claimA window $w$ is neutral when its signed sum vanishes: $isNeutralWindow(w) := (signedSum(w) = 0)$. The eight-tick neutrality predicate implies exact closure, and the associated gap weight $w_8$ is unique and positive.
background
Recognition Science organizes measurement around the eight-tick octave (T7) whose period is $2^3$. The GapWeight module supplies the single parameter-free coefficient $w_8$ appearing in the gap term $f_{gap} = w_8 · ln(φ)$ of the α pipeline. The Patterns module provides the underlying recognition objects on which signed sums are evaluated. WindowNeutrality sits in the Measurement domain and introduces the neutrality predicate that detects exact rests without external tuning.
proof idea
This is a definition module, no proofs. The central object is the predicate isNeutralWindow whose body is the signed-sum condition. The remaining declarations are one-line wrappers or direct algebraic consequences that establish the exactness implication, uniqueness of $w_8$, and positivity of the gap weight.
why it matters in Recognition Science
The module supplies the eight-window neutrality predicate consumed by the PeriodicTable engine to identify noble-gas closures. It completes the measurement-to-chemistry interface in the fit-free scaffold, allowing downstream predictions to remain parameter-free while respecting the eight-tick structure of the forcing chain.
scope and limits
- Does not assign numerical masses or energies to specific elements.
- Does not incorporate experimental data or fitting procedures.
- Does not extend the neutrality predicate beyond eight-tick windows.
- Does not claim uniqueness outside the signed-sum definition.