Add linear geometry, sphere, SO(n), and quaternion type core

[isomorphisms]

Scope

Bounded second-pass type-system slice centered on finite-dimensional linear algebra and standard geometry. This is stacked on #44 (examples/units-time-intervals) so this PR's diff is geometry-only.

Dimensioned linear algebra / semantic embeddings

• ExactRealVector n makes ambient dimension a type index;
• subtraction, dot product, norm, distance, and semantic residual require the same dimension by construction;
• approximation thresholds stay explicit rather than being guessed by the compiler.

The executable coordinate samples use integers embedded in R^n so the tests are exact and do not choose a floating-point policy. This is not a claim that real coordinates are integers.

O(n), SO(n), rotations, reflections

• orientation is a type index (Preserving / Reversing);
• reflection × reflection reduces to an SO(n) result type;
• there is no arbitrary constructor that simply asserts a matrix is orthogonal;
• first exact generators are a coordinate-axis reflection and a first-plane quarter turn (Givens c=0,s=1);
• general-angle/arbitrary-axis realizations remain open until the scalar/trig layer is settled.

Spheres

• UnitSpherePoint n means S^n in ambient R^(n+1);
• O(n+1) actions preserve sphere membership at the type boundary;
• integral cohomology ranks are encoded, including the special S^0 case;
• parity is recorded through chi(S^n)=1+(-1)^n (odd 0, even 2), without falsely claiming odd/even spheres have different additive cohomology ranks.

Quaternions / SO(3)

• Hamilton multiplication and squared norm on exact integer-coordinate quaternion samples;
• norm-one dependent certificates;
• typed unit-quaternion -> SO(3) boundary.

CP^n / standard topology facts

• real dimension 2n;
• Hopf presentation sphere dimension for CP^n = S^(2n+1)/S^1;
• additive integral cohomology ranks;
• named theorem-library facts for Jordan separation on S^2 and (R^n)^+ ~= S^n one-point compactification.

The last items model the intended #42 theorem-index boundary: named checked facts may contribute typed consequences; the compiler is not pretending to rediscover their proofs.

Tests-first history

• tests first: f799d79663f320a26421a9f2a24207de3af540d3
• implementation: 97951746363b9ee7e6c4b9b9470fde5dbbeff768
• compiler harness: edric008, added to ./edric test
• golden-newline correction after first real run: 6b46694b26328ae4b71134ce8b52bdb8c00fb4e8

Deliberately deferred

General real-scalar representation, arbitrary Householder/Givens parameters, imported-matrix orthogonality certification, subspaces/projections, full CP^n quotient equality, the cohomology ring, and theorem-provenance machinery.

Verification

The first real compiler run (#8) successfully compiled and executed edric008 and produced exactly linear geometry type core: ok. The workflow failed only because the committed golden file lacked the executable's terminal newline. No mathematical/type test failed and no implementation weakening was needed. Commit 6b46694b26328ae4b71134ce8b52bdb8c00fb4e8 fixes that one-byte golden mismatch.

Exact-head Edric type-system smoke run 33278264928 and Edric wrapper run 33278264952 both passed. The compiler receipt and whole workflow are green at 6b46694b26328ae4b71134ce8b52bdb8c00fb4e8.

Related: #42, #44.

Competing mathematical model

#44 → #45 → #47 is one strict experimental stack. Independent PR #46 uses a different model: this branch has rank-indexed Euclidean coordinate vectors and a direct dot product, while #46 has nominally named spaces and permits contraction only between Covector space and Vector space, with no implicit metric. Both currently occupy tests/idris2/basic/edric008, so choosing between them is not a mechanical merge.

[isomorphisms]

I split the requested high-dimensional rotation/reflection verification onto a fresh stacked branch, examples/high-dimensional-orthogonal-tests, so the already-running #45 geometry smoke stays untouched. Tests-first commit: 1b28c6fb07803d233ef976caf483cce345ae6fe6. The new fixtures instantiate the generic O(n)/SO(n) constructors at R^128 and demand exact coordinate images, norm/dot preservation, reflection involution, and four-quarter-turn identity before adding their coordinate realization.

[isomorphisms]

Classification: SUPERSEDED by #51.

#51 preserved the useful geometry line through the reconciled named-space/Euclidean model, including orthogonal and special-orthogonal structure, sphere/CPn topology facts, and the sound theorem boundary.

#51 deliberately did not retain the unchecked certified sphere-action wrapper. No unique implementation from this PR remains pending here; the discussion remains useful historical context for the reconciliation.