PhaseParams
plain-language theorem explainer
PhaseParams supplies the coprime moduli 8 and 45 that frame double-period phasing inside eight-tick temporal gating. Researchers constructing feasibility predicates for angular and temporal admissibility in Recognition Science cite this structure. The definition is a direct record whose coprimality field is discharged by the decide tactic.
Claim. The structure PhaseParams is the record with fields $a : ℕ := 8$, $b : ℕ := 45$, and the proposition that $a$ and $b$ are coprime.
background
The Temporal Gating module abstracts the discrete sampling windows of the eight-tick octave and defines a feasibility predicate that merges an angular threshold with temporal admissibility. The upstream tick definition sets the fundamental time quantum, with one octave equal to eight ticks. The phase definition from EightTick supplies the discrete phases $kπ/4$ for $k = 0,…,7$. This structure provides the coprime moduli pair for double-period phasing.
proof idea
The structure is defined by supplying default values 8 and 45 for the two moduli together with a coprimality proof that the decide tactic discharges.
why it matters
This definition provides the parameter record required by the feasibility predicates in the same module, which implement the eight-tick octave of the forcing chain (T7). It supports the construction of admissible phase windows for measurement in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.