pith. sign in
def

neutral8

definition
show as:
module
IndisputableMonolith.Foundation.Breath1024
domain
Foundation
line
30 · github
papers citing
4 papers (below)

plain-language theorem explainer

The eight-tick neutrality predicate asserts that a real-valued function on the naturals sums to zero over any eight consecutive ticks. Physicists modeling periodic oscillators in the Recognition framework cite this when imposing neutrality constraints on period-8 streams. It is introduced by a direct equational definition that reduces the predicate to the vanishing of the pre-defined eight-window summation operator.

Claim. The predicate that a function $x : T → ℝ$ is neutral at starting tick $t_0$ holds precisely when the sum of $x$ over the eight consecutive ticks beginning at $t_0$ equals zero, where $T = ℕ$.

background

The Breath1024 module treats oscillator records whose generative and radiative streams are assumed periodic with periods 8 and 1024. T is the abbreviation for the natural numbers serving as the discrete time domain. The sibling sum8 returns the sum of function values over the eight-tick window starting at a given point, with the comment labeling it the eight-window neutrality predicate. An upstream definition in Astrophysics.PulsarEmissionRegimesFromRS sets period(k) = phi^k, supplying the scaling that aligns with the self-similar fixed point.

proof idea

This is a one-line definition that directly equates the predicate to the proposition that the eight-window sum equals zero, using the already-defined sum8 operator.

why it matters

It encodes the neutrality condition over the eight-tick octave required at step T7 of the unified forcing chain. The predicate is referenced by the neutral8 constructions in Chemistry.EnvPressure and Crystallography.SelectionRules, which apply the same window-sum idea to pressure and selection-rule models. It supplies the basic interface layer for the Breath1024 oscillator record and supports downstream use in nuclear octave and gap-minimization contexts.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 4 of 4)