pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Measurement.WindowNeutrality

show as:
view Lean formalization →

WindowNeutrality defines the predicate for neutral eight-tick measurement windows in Recognition Science. A window is neutral precisely when its signed sum vanishes. The module supplies this condition to the PeriodicTable engine for locating noble-gas closures on the phi-ladder. It imports gap-weight and pattern definitions to keep the construction parameter-free. The module consists of definitions and supporting lemmas rather than extended proofs.

claimA window $W$ is neutral when its signed sum vanishes: $s(W) = 0$. The gap weight satisfies $f_{gap} = w_8 ln phi$ with $w_8$ fixed by the 8-tick projection.

background

Recognition Science organizes measurements inside eight-tick octaves that arise from the self-similar fixed point phi. The imported GapWeight module supplies the single gap term $f_{gap} = w_8 ln phi$, where $w_8$ is required to be parameter-free and closed-form. The Patterns module provides the structural templates that these windows act upon. Window neutrality is the zero-sum condition that closes periodic structures without external tuning.

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 the PeriodicTable engine. That downstream module maps octaves to phi-tier rails and uses neutrality to detect noble-gas closures. It thereby advances the zero-parameter scaffold for chemistry by enforcing the signed-sum condition on the eight-tick structure.

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)