Cost Ndim Octave Octave Trajectory

The octave trajectory

An octave trajectory is a plain cosine wave: for each of eight equally spaced phase shifts, the value is amplitude times the cosine of time plus that shift. In symbols, the i-th component is amp * cos(t + 2πi/8). Because cosine repeats every 2π, the whole eight-component curve returns to its starting state after that interval. The machine-checked theorem octaveTrajectory_periodic proves exactly that periodicity: shifting the input by 2π leaves the output unchanged.

The eight phases divide the circle into equal eighths, so the trajectory traces the same shape as a point moving around a circle, sampled at eight evenly spaced angles. This is a visualization aid, not a physical law. It shows how a recognition cycle, the framework's term for a discrete record of eight stages, might be drawn as a smooth repeating wave. The definition chooses the cosine form and the phase spacing; nothing about the real world follows from that choice alone.

In Recognition Science, the framework's library of formal theorems uses this trajectory to illustrate the eight-tick cycle that its forcing chain derives. The chain proves that a certain cost function must equal J(x) = (x + 1/x)/2 - 1, and from that forces the golden ratio and an eight-stage cycle. The octave trajectory is a picture of that cycle, not a proof of it. The periodicity theorem is real, but it only states a property of the chosen cosine formula.

What the declaration does not claim: it does not say that the octave trajectory is the only possible shape for the cycle, nor that the cycle itself is physically real. The trajectory is a definition, not a derivation. The forcing chain that produces the eight-tick cycle is separate; the trajectory merely visualizes it. A reader should take the periodicity as a mathematical fact and the visualization as a helpful picture, with no further commitment.

/-- Phase-shifted cosine trajectory used in the `n=8` visualization. -/
noncomputable def octaveTrajectory (amp t : ℝ) : Vec 8 :=
  fun i => amp * Real.cos (t + octavePhase i)

theorem octaveTrajectory_periodic (amp t : ℝ) :
    octaveTrajectory amp (t + 2 * Real.pi) = octaveTrajectory amp t := by
  ext i
  unfold octaveTrajectory
  have hrew : t + 2 * Real.pi + octavePhase i = (t + octavePhase i) + 2 * Real.pi := by ring
  calc
    amp * Real.cos (t + 2 * Real.pi + octavePhase i)
        = amp * Real.cos ((t + octavePhase i) + 2 * Real.pi) := by rw [hrew]
    _ = amp * Real.cos (t + octavePhase i) := by
          rw [Real.cos_add_two_pi]

What this page does not claim

The octave trajectory is not a derived physical law; it is a chosen definition. The periodicity theorem does not imply that recognition cycles are real or that they follow a cosine shape. The eight-tick cycle itself is not proved by this declaration; it comes from a separate forcing chain.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/Octave.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: