R3
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.