exists_feasible_if_angleOK_and_time_slot
plain-language theorem explainer
If the angular threshold holds for vectors x, y, z in Euclidean 3-space with amplitude bound Amax and there exists an admissible integer time slot under eight-tick parameters p, then a feasible configuration exists for some integer n. Measurement theorists working on discrete temporal gating would cite this to guarantee existence of admissible events under combined geometric and temporal constraints. The proof is a direct term-mode extraction that destructures the existential time-slot hypothesis and assembles the witness via conjunction.
Claim. Let $x,y,z$ be vectors in Euclidean 3-space and let $A_0$ be a real amplitude bound. Let $p$ be eight-tick parameters (a phase in the 8-cycle together with a nonempty admissible window set). If the angle condition holds for $x,y,z,A_0$ and there exists an integer $n$ such that the time slot $n$ is admissible for $p$, then there exists an integer $n$ for which the configuration is feasible under $p$ and $A_0$.
background
R3 denotes Euclidean 3-space. EightTickParams is the structure carrying a phase in Fin 8 and a nonempty set of admissible windows; it encodes the discrete eight-tick gating windows of the module. The local setting abstracts these windows and defines a feasibility predicate that conjoins the angular threshold with temporal admissibility. Upstream results supply the angleOK predicate (from BlindCone and ActionSmallAngle) together with the local timeOK and feasible predicates that appear in the hypotheses.
proof idea
The term-mode proof applies rcases to the existential hypothesis hslot, obtaining a witness n and a proof hn that timeOK n p holds. It then returns the pair consisting of that n together with the conjunction of the angle hypothesis hθ and hn.
why it matters
The result supplies the basic existence step used by the downstream trivialParams definition, which shows that any angle-OK configuration is feasible under a universal window. It fills the temporal-gating link in the recognition-angle measurement layer and connects to the eight-tick octave (T7) of the forcing chain. It touches the discrete-sampling aspect of the Recognition Science measurement framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.