power_of_two
power_of_two maps a natural number D to 2 raised to that power. Researchers tracing the eight-tick octave through the Gap45 derivation cite it when showing that D equals 3. The definition is introduced as a direct abbreviation of exponentiation, so the equality at D=3 holds by reflexivity.
claimFor a natural number $D$, define the power of two by $2^D$.
background
The Gap45.Derivation module shows that 45 arises from the eight-tick structure (T8) combined with the Fibonacci sequence tied to phi. The module states 45 equals (8+1) times 5, where the factor 8 is supplied by 2^D at D=3 and the extra 1 encodes closure of one full cycle. This construction treats 45 as the ninth triangular number T(9), representing cumulative phase accumulation over the closed eight-tick period.
proof idea
The declaration is a direct definition that invokes Lean's built-in natural-number exponentiation operator.
why it matters in Recognition Science
The definition supplies the concrete value 8 that appears in the downstream theorem D_3_gives_8. That theorem closes the step linking T8 to three spatial dimensions, confirming the factorization 45 = 9 times 5 and the relation lcm(8,45)=360 that forces D=3 in the Recognition Science forcing chain.
scope and limits
- Does not prove any arithmetic identities for 2^D beyond the definition itself.
- Does not derive the value of D from any physical equation.
- Does not reference the Recognition Composition Law or mass ladder formulas.
Lean usage
theorem D_3_gives_8 : power_of_two 3 = 8 := rflformal statement (Lean)
151def power_of_two (D : ℕ) : ℕ := 2^D
proof body
Definition body.
152
153/-- lcm(2^D, 45) = 360 only when D = 3. -/