octave_offset
plain-language theorem explainer
The octave offset is defined as the negation of T_min(D), the Hamiltonian cycle period on the three-cube. Mass ladder work in Recognition Science cites this to fix the vacuum rung at negative eight. It is a direct abbreviation that applies the cube vertex count from T_min and casts the result to integers.
Claim. Let $T_0(d)$ be the Hamiltonian cycle period on the $d$-cube, equal to its vertex count $2^d$. The octave offset is defined by $o := -T_0(D)$ with $D=3$.
background
The Baseline Rung Derivations module upgrades prior boundary assumptions to derived status by tracing every integer to the single input D=3 and the combinatorics of the 3-cube Q_3. T_min(d) is defined as the vertex count of the d-cube and equals the period of a Hamiltonian cycle on that cube; the module records that this period is 8 when d=3. The local setting therefore treats the vacuum rung as one complete cycle period, with the octave offset supplying the signed integer shift required for the phi-ladder.
proof idea
One-line definition that applies T_min to D, casts the natural number to an integer, and negates the result.
why it matters
The definition supplies the octave offset used by the theorem octave_offset_eq that establishes the concrete value -8. It fills the B-15 slot among the derived baseline rungs. In the Recognition framework it realizes the eight-tick octave (period 2^3) at D=3 and anchors the vacuum rung for subsequent mass formulas on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.