octave_offset_eq
plain-language theorem explainer
The equality establishing the octave offset equals negative eight follows from unfolding the definitions of the octave offset, minimum tick count T_min, cube vertex count, and spatial dimension D, then normalizing the arithmetic. Researchers deriving baseline rungs on the Recognition Science phi-ladder cite this result to anchor the zero point for D equal to three. The proof reduces the claim to a numerical identity via direct unfolding and norm_num.
Claim. Let $T_{min}$ denote the minimum tick count on the $D$-cube. The octave offset, defined as the negative of $T_{min}$, satisfies octave_offset = $-8$ when $D=3$.
background
The Baseline Rung Derivations module upgrades previously assumed boundary items to derived status by extracting structural integers from the combinatorics of the three-cube Q_3. The octave offset is defined as the negative of T_min, where T_min equals the vertex count supplied by the cube_vertices function. The module documentation states that every integer traces to the single input D equals three, with the table listing B-15 as octave offset equals negative T_min equals negative 2 to the D, evaluating to negative eight.
proof idea
The proof is a one-line wrapper that unfolds the definitions of octave_offset, T_min, cube_vertices and D, then applies norm_num to reduce the equality to a numerical identity.
why it matters
This result supplies the octave offset required by the neutrino_rung theorem in the same module. It fills item B-15 in the derivation table and confirms the eight-tick octave (period 2^3) for D equals three required by the T7 step of the Unified Forcing Chain. The downstream neutrino baseline theorem relies on this geometric count together with related cube integers to fix the neutrino rung at negative fifty-four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.