pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Octave

show as:
view Lean formalization →

The module defines uniform phase shifts for octave indices and associated trajectories in the N-dimensional reciprocal cost model. It equips the eight-tick octave structure with phase and periodic trajectory functions that extend the scalar cost kernel. Researchers working on multi-dimensional defect dynamics or the phi-ladder would reference these when building periodic extensions. The module contains only definitions and imports the Core module without any theorems.

claimUniform phase shift function for octave index $n$, written $phase(n)$, together with trajectory function $trajectory(t,n)$ satisfying the periodicity condition $trajectory(t+8,n)=trajectory(t,n)$.

background

The module sits inside the Cost domain of Recognition Science and imports the Core module, which defines the N-dimensional reciprocal cost by lifting the scalar J-cost kernel through a weighted log aggregate. It formalizes the octave concept from the T7 step of the forcing chain, where the period is fixed at eight ticks to support self-similar scaling under the phi fixed point. The supplied doc-comment states the central object is the uniform phase shift for an octave index, providing the phase and trajectory primitives needed for composing costs across octave rungs.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the phase and trajectory machinery required by the T7 eight-tick octave in the UnifiedForcingChain, which in turn forces D=3 spatial dimensions at T8. They enable periodic extensions of the reciprocal cost that feed into downstream calculations of the alpha band and the phi-ladder mass formula. No used-by edges are recorded, yet the module closes the scaffolding gap between the Core cost aggregate and any higher-level periodic composition law.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)