Pith. sign in
module module high

IndisputableMonolith.Measurement.WindowNeutrality

show as:
view Lean formalization →

This module defines window neutrality for the Recognition Science measurement layer: a window counts as neutral exactly when the algebraic sum of its signed contributions is zero. It supplies the predicate required by the Periodic Table engine to mark noble-gas closures on the phi-ladder. The module is a short collection of definitions and elementary lemmas built directly on the eight-tick structures imported from Patterns and GapWeight.

claimA measurement window is neutral when the signed sum of its eight contributions vanishes: $\sum_{k=1}^{8} \sigma_k = 0$.

background

Recognition Science organizes periodic structure through the eight-tick octave (T7) and the phi-ladder. GapWeight supplies the single parameter-free gap weight $w_8$ used in the alpha pipeline via $f_{\rm gap}=w_8\ln\phi$. Patterns supplies the underlying combinatorial objects. The present module adds the neutrality predicate that detects exact cancellation inside any such eight-tick window.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the eight-window neutrality predicate required by IndisputableMonolith.Chemistry.PeriodicTable to identify rests (noble-gas closures) on the phi-tier rails. It thereby completes the zero-parameter measurement interface for the chemistry scaffold and directly implements the eight-tick neutrality needed for the octave mapping.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)