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

IndisputableMonolith.Cost.Ndim.Octave

show as:
view Lean formalization →

This module defines uniform phase shifts indexed by octaves within the N-dimensional reciprocal cost framework. It extends the scalar kernel lifting from the Core submodule to handle periodic eight-tick structures. The module contains only definitions and no theorems or proofs.

claimThe module supplies the uniform phase shift function $f(k)$ for octave index $k$, together with trajectory maps that satisfy $f(k+8)=f(k)$ over the eight-tick cycle.

background

The module sits in the Cost domain and imports the Core submodule, whose doc-comment states that it defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. This supplies the J-cost and defectDist primitives used for N-dimensional extensions. The octave index directly references the eight-tick period (T7) in the forcing chain, where phase is required to be uniform.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the phase and trajectory objects required by the eight-tick octave step (T7) of the UnifiedForcingChain. They prepare periodic structures that later feed into D=3 spatial constructions and the Recognition Composition Law. No downstream theorems are recorded in the current dependency graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)