pith. machine review for the scientific record. sign in
def definition def or abbrev high

feasible

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  41def feasible (x y z : R3) (Amax : ℝ) (p : EightTickParams) (n : ℤ) : Prop :=

proof body

Definition body.

  42  angleOK x y z Amax ∧ timeOK n p
  43
  44/-! ## Basic feasibility theorems (parameterized) -/
  45
  46/-- If the geometric threshold fails, no event index is feasible (for any gating params). -/

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.