Osc
plain-language theorem explainer
Osc pairs two real-valued functions g and r over the natural numbers T to represent generative and radiative streams in the Breath1024 oscillation model. Researchers formalizing phase-lag relations in Recognition Science cite this structure when stating fixed-shift predicates such as the 512-tick flip. The declaration is a bare structure with no proof obligations or computational content.
Claim. An oscillator is a pair of functions $g, r : T → ℝ$, where $T$ is the type of fundamental periods.
background
T is an abbreviation for the natural numbers ℕ and stands for the set of fundamental periods in the Breath1024 module. The structure is introduced in a module that also imports the triangular-number definition T(n) = n(n+1)/2 from Gap45.SyncMinimization, though that definition is not used inside Osc itself.
proof idea
The declaration is a direct structure definition that introduces the two fields g and r with no lemmas or tactics applied.
why it matters
Osc supplies the input type for flipAt512, which asserts that the radiative stream equals the generative stream shifted by flipTick, and for phaseLagPiOver4, which encodes the sinusoidal forms with a π/4 phase offset. It therefore anchors the period-1024 analysis that supports the eight-tick octave construction in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.