phaseLagPiOver4
plain-language theorem explainer
The predicate asserts that an oscillator's radiative component equals the sine of frequency times time plus π/4 while the generative component equals the plain sine, for all discrete times in the fundamental period. Analysts of synchronization in the Breath1024 construction of Recognition Science would invoke this predicate when checking phase relations inside the eight-tick octave. The definition is a direct universal quantification over the natural-number time domain with no auxiliary lemmas.
Claim. For frequency $ω ∈ ℝ$ and oscillator $O$ with generative map $g : ℕ → ℝ$ and radiative map $r : ℕ → ℝ$, the predicate holds if and only if $∀ t ∈ ℕ$, $r(t) = sin(ω t + π/4)$ and $g(t) = sin(ω t)$.
background
Breath1024 works inside the Recognition Science foundation by encoding periodic streams over 1024 ticks built from an eight-tick octave. The Osc structure supplies the two streams: generative component $g$ and radiative component $r$, each a function from the fundamental period $T = ℕ$ into the reals. The predicate therefore fixes a concrete phase offset between those streams.
proof idea
The definition is a direct encoding: it simply writes the required equality of the two components to the sine expressions with the π/4 offset, universally quantified over all $t$ in $T$. No lemmas from the depends-on list are invoked; the body is the predicate itself.
why it matters
The predicate supplies the exact phase relation needed to instantiate oscillators inside the Breath1024 module, supporting the eight-tick octave (T7) and the period-1024 constructions listed among its siblings. It sits at the foundation level before any downstream synchronization theorems are stated, consistent with the Recognition Composition Law and the phi-ladder timing conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.