rsDimension_eq_3
plain-language theorem explainer
The declaration confirms that the recognition dimension equals three by reflexivity on its local definition. Linear algebra constructions in the Recognition Science framework cite it to fix D = 3 when building the F₂³ lattice and the five canonical operations. The proof succeeds because rsDimension is defined as the numeral 3 in the same module, so the equality holds definitionally.
Claim. The recognition dimension satisfies $D = 3$.
background
The module equips the recognition lattice with a linear algebra structure over the reals. The central parameter is the recognition dimension, introduced as a natural number that equals the spatial dimension D. The module documentation states that the D=3 recognition space is ℝ³, with three basis vectors, an orthogonal complement of dimension three, and the F₂³ lattice of cardinality 8 matching the recognition period.
proof idea
The proof is a one-line reflexivity step (rfl) on the definition of rsDimension, which is set to 3 in the same file. No lemmas from the upstream rsDimension declarations in DifferentialGeometryFromRS or SuperstringTheoryFromRS are invoked; the equality is immediate from the local definition.
why it matters
The result supplies the dimension_3 field inside the linearAlgebraCert definition that certifies the five operations, dimension 3, and F₂³ size 8. It directly implements the T8 step of the unified forcing chain that forces three spatial dimensions. The declaration ensures consistency of the D=3 value across the mathematics and physics modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.