pith. sign in
def

flipAt512

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

plain-language theorem explainer

flipAt512 encodes a phase-lag predicate on an Osc pair, requiring the radiative function r at time t plus 512 ticks to equal the generative function g at t. Researchers modeling eight-tick octave dynamics or Breath1024 breath cycles in Recognition Science would cite this diagnostic when checking fixed shifts between generative and radiative streams. The definition is a direct universal quantification over the time domain using the pre-defined flipTick constant.

Claim. For an oscillator $O$ with generative map $g:T→ℝ$ and radiative map $r:T→ℝ$, the predicate holds if and only if $r(t+512)=g(t)$ for all $t∈T$.

background

Osc is the structure pairing generative and radiative real-valued functions on the time domain T. flipTick is the constant 512, half the 1024-period breath cycle. Upstream constants fix one octave as 8 ticks and link the construction to phi-forcing derived quantities and ledger factorization.

proof idea

The definition is a direct encoding of the shift condition on the Osc fields using the flipTick constant; no lemmas or tactics are invoked beyond the structure projection and the numeric literal.

why it matters

The predicate supplies a diagnostic check inside the Breath1024 module for phase relations governed by the eight-tick octave (T7). It sits alongside octave definitions from MusicalScale and Constants but has no recorded downstream uses, leaving open how the 512-tick shift maps onto the π/4 lag stated in the module comment.

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

papers checked against this theorem (showing 11 of 11)