pith. machine review for the scientific record. sign in
def definition def or abbrev high

comp

show as:
view Lean formalization →

This definition equips the collection of octaves with morphism composition by taking the composite of their underlying state maps and chaining the order-preservation properties. Researchers building chains of transformations for the J-action convexity theorem or energy conservation results cite it when assembling longer sequences of octave maps. The construction is a direct structural definition that reuses the preservation axioms of the two input morphisms in sequence.

claimLet $O_1, O_2, O_3$ be octaves. Given morphisms $g: O_2 → O_3$ and $f: O_1 → O_2$ that each preserve the weak ordering induced by their strain functionals, the composite morphism $g ∘ f: O_1 → O_3$ is defined by the state map $g.map ∘ f.map$ and satisfies the preservation property because if $x$ is weakly better than $y$ under the strain of $O_1$, then $f.map(x)$ is weakly better than $f.map(y)$ under the strain of $O_2$, and therefore $g.map(f.map(x))$ is weakly better than $g.map(f.map(y))$ under the strain of $O_3$.

background

An octave is an abstract state space equipped with a strain functional (the J-cost), a bundle of display channels, and a non-emptiness witness. A morphism between octaves is a function on states that preserves the weak ordering induced by the respective strain functionals: if one state is weakly better than another in the source octave, its image is weakly better in the target octave. The present module develops this structure purely abstractly, without imposing concrete scaling factors or the eight-tick period that appear only in later hypotheses.

proof idea

The definition constructs the target OctaveMorphism by setting its map field to the ordinary function composition of the two input maps and its preserves_order field to the lambda that first applies the source morphism's preservation and then the target morphism's preservation. No external lemmas are invoked; the proof is the direct structural assembly of the two given preservation axioms.

why it matters in Recognition Science

The definition supplies the categorical composition operation required to form chains of octave morphisms that feed the convexity theorem for the J-action and the energy-conservation theorem for Newtonian trajectories. It completes the basic algebraic infrastructure of the RRF core before any physical constants or the phi-ladder are introduced, and it is mirrored by the composition operation already present in the cost-algebra layer.

scope and limits

formal statement (Lean)

  67def comp {O₁ O₂ O₃ : Octave}
  68    (g : OctaveMorphism O₂ O₃) (f : OctaveMorphism O₁ O₂) : OctaveMorphism O₁ O₃ where
  69  map := g.map ∘ f.map

proof body

Definition body.

  70  preserves_order := fun x y h => g.preserves_order _ _ (f.preserves_order x y h)
  71
  72/-- Morphisms preserve equilibria (if target has NonNeg strain). -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (11)

Lean names referenced from this declaration's body.