phiPatternComplex
plain-language theorem explainer
The eight-tick φ-power sequence is lifted from reals to complexes by the standard embedding, so discrete Fourier analysis can act on it. Anyone computing DFT coefficients or mode amplitudes of the canonical φ-pattern cites this cast. The body is a one-line pointwise coercion of the real φ-pattern.
Claim. Define the complex eight-tick $\varphi$-pattern by $t \mapsto (\varphi^{t} : \mathbb{C})$ for $t \in \{0,\ldots,7\}$, i.e. the pointwise complexification of the real samples $\varphi^{t}$.
background
The module fixes the canonical $\varphi$-pattern on the eight-tick window: real samples $\varphi^{t}$ for $t \in \mathrm{Fin},8$. That length matches the Recognition Science eight-tick octave (forcing step T7, period $2^{3}$).
DFT analysis in the imported eight-point spectral layer needs complex-valued signals. The real pattern is therefore embedded into $\mathbb{C}$ by the usual ring homomorphism $\mathbb{R}\to\mathbb{C}$. No new numerical content is introduced; only the codomain changes so that star-products with DFT matrix entries are well-typed.
Upstream, the real pattern is exactly $t \mapsto \varphi^{t.val}$. Sibling Pattern abbreviations elsewhere in the codebase are Boolean windows and are not used here; the relevant object is the real $\varphi$-power sequence.
proof idea
Definitional one-liner: at each $t:\mathrm{Fin},8$, coerce the real value of the $\varphi$-pattern to $\mathbb{C}$. No lemmas, no tactics, no arithmetic. The noncomputable flag is inherited from $\varphi$ and real exponentiation.
why it matters
This cast is the input to the DFT coefficient $c_k$ of the $\varphi$-pattern, formed as $\sum_t \overline{(\mathrm{DFT}8){t k}}\cdot(\text{complex $\varphi$-pattern})_t$. Squared amplitudes of those coefficients feed the geometric and DFT-based gap-weight candidates, including the positivity theorem for the DFT weight candidate.
In the Recognition framework the eight-tick $\varphi$-ladder is the discrete skeleton behind gap weights and mass-ladder bookkeeping. Complexifying the pattern is the minimal bridge from the real $\varphi$-powers to spectral mode weights used in constant formulas. It does not itself force $\varphi$ or the octave length; those sit upstream in the forcing chain (T6, T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.