feasible
plain-language theorem explainer
Combined feasibility predicate for event index n under eight-tick gating. It is cited in determinism and variational-dynamics proofs when establishing reachable ledger states from angular and temporal constraints. The definition is a direct conjunction of the angleOK predicate on R3 vectors with the timeOK predicate on the integer index and gating parameters.
Claim. Let $x,y,z$ be vectors in Euclidean space $R^3$, let $A_{max}$ be a real amplitude bound, let $p$ be an EightTickParams structure (phase in Fin 8 together with a nonempty admissible window set), and let $n$ be an integer. The predicate holds exactly when the angular threshold on $x,y,z,A_{max}$ is met and the temporal admissibility condition on $n$ and $p$ holds.
background
The TemporalGating module abstracts discrete eight-tick sampling windows and supplies a feasibility predicate that merges an angular threshold with temporal admissibility. R3 is the abbreviation for EuclideanSpace R (Fin 3). EightTickParams is the structure carrying a phase in Fin 8 and a nonempty Set (Fin 8) of admissible windows.
proof idea
One-line definition that packages the conjunction of angleOK x y z Amax and timeOK n p. No lemmas are invoked; the body simply assembles the two sibling predicates already defined in the same module.
why it matters
The predicate is invoked by the unique-minimizer principle and the IsEquilibrium definition inside VariationalDynamics, and by the satisfiable-iff-linearFeasible equivalence in the BWD3 SAT closure. It supplies the temporal component of the eight-tick octave (T7) that, together with the R3 spatial structure, enforces deterministic reachability in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.