`Octave`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Core.Octave
domain: RRF
line: 29 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Core.Octave on GitHub at line 29.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  26This is the abstract structure; no physical constants (φ, 8-tick) here.
  27Those are hypotheses layered on top.
  28-/
  29structure Octave where
  30  /-- The state space at this octave. -/
  31  State : Type*
  32  /-- The strain functional (J-cost). -/
  33  strain : StrainFunctional State
  34  /-- Display channels available at this octave. -/
  35  channels : ChannelBundle State
  36  /-- Non-emptiness: at least one state exists. -/
  37  inhabited : Nonempty State
  38
  39namespace Octave
  40
  41variable (O : Octave)
  42
  43/-- The equilibrium states of an octave. -/
  44def equilibria : Set O.State := O.strain.equilibria
  45
  46/-- An octave is well-posed if it has at least one equilibrium. -/
  47def wellPosed : Prop := ∃ x : O.State, O.strain.isBalanced x
  48
  49end Octave
  50
  51/-- A morphism between octaves: a map that preserves strain ordering. -/
  52structure OctaveMorphism (O₁ O₂ : Octave) where
  53  /-- The underlying map on states. -/
  54  map : O₁.State → O₂.State
  55  /-- The map preserves strain ordering. -/
  56  preserves_order : ∀ x y, O₁.strain.weaklyBetter x y →
  57                           O₂.strain.weaklyBetter (map x) (map y)
  58
  59namespace OctaveMorphism

papers checked against this theorem

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