`phaseLagPiOver4`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.Breath1024
domain: Foundation
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.Breath1024 on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  42
  43/‑ Fixed phase‑lag predicate (diagnostic): r leads g by π/4 on each octave.
  44   Here represented at the level of a simple sinusoidal probe (display‑only). -/
  45def phaseLagPiOver4 (ω : ℝ) (O : Osc) : Prop :=
  46  ∀ t : T,
  47    O.r t = Real.sin (ω * (t : ℝ) + Real.pi / 4) ∧
  48    O.g t = Real.sin (ω * (t : ℝ))
  49
  50end Breath1024
  51end Foundation
  52end IndisputableMonolith
  53
  54
  55
  56
  57
  58
  59
  60

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.