R3
R3 supplies the three-dimensional Euclidean space that hosts all direction vectors and angular computations in the recognition-angle module. Researchers formalizing sensor geometry or action kernels in the Recognition Science setting would reference it when stating positions and separations. The declaration is a direct type abbreviation with no additional lemmas or reductions.
claimLet $R^3$ denote the three-dimensional real Euclidean space equipped with the standard inner product.
background
The module supplies the geometric primitives for the recognition-angle program. R3 is introduced as the ambient space for positions, with sibling definitions for the angle at a vertex between two rays and the kernel action expressed as a function of that angle. Upstream, the alias depends on the structural conditions extracted from seven axioms in PrimitiveDistinction and on identical R3 aliases already present in the BlindCone and TemporalGating modules.
proof idea
The declaration is a direct one-line abbreviation that specializes the Mathlib EuclideanSpace type to dimension three via Fin 3.
why it matters in Recognition Science
R3 is referenced by the ten downstream declarations that define unit directions, compute angles, construct blind cones, and state angle-admissibility predicates. It supplies the concrete three-dimensional setting required by the forcing chain at T8. The alias thereby closes the geometric layer needed for the subsequent feasibility theorems in TemporalGating.
scope and limits
- Does not introduce a preferred basis or coordinate chart.
- Does not extend the metric beyond the standard Euclidean structure.
- Does not assign physical units or scaling to vectors in the space.
- Does not restrict points to any discrete subset or lattice.
formal statement (Lean)
29abbrev R3 := EuclideanSpace ℝ (Fin 3)
proof body
Definition body.
30
31/-- Unit direction from `x` to `y` in `R3`; returns `0` on degeneracy. -/