Reconcile higher-mathematics space semantics

[isomorphisms]

Summary

• unify named finite spaces and known rank by indexing each SpaceName with its unique rank
• keep ExactVectorSample and ExactCovectorSample distinct, with checked contraction and an explicit Raw.../Unsafe... fixture boundary
• require EuclideanStructure for lowering/raising, dot products, norms, distances, and the closed O/SO model
• interpret the same closed orthogonal-transform syntax that carries orientation, preserving the exact strengthened R^128 reflection and quarter-turn oracle from Test exact high-dimensional rotations and reflections #47
• keep the finite presheaf restriction model separate while retaining its typed identity, composition, and componentwise laws
• preserve the sound sphere/CP^n/topology facts and add one tiny typed, provenance-labelled named-fact application boundary for Infer higher-math structures from operations, laws, and theorem constraints #42/Classify .idric sources as Idris on GitHub #56

The branch is intentionally tests-first: the first commit specifies the unified model and fixture; the second implements it.

Verification

Exact tested PR tip: 7760db10b6e53148491d7380f0fa846049819bdc

• ./edric bootstrap — PASS (real bootstrapped Idric compiler path)
• ./edric test --only idris2/basic/edric009 — PASS, 1/1
• ./edric test — PASS for edric001 through edric006 and edric009
• python3 examples/unified-higher-mathematics/verify_r128.py — 13/13 secondary exact checks PASS

The focused fixture preserves the .idric suffix and avoids the two historical edric008 fixtures colliding.

Mathematical boundary

This does not implement a complete real-scalar carrier, arbitrary matrix certification, general cohomology, quotient construction, theorem search, or a theorem prover. A certified UnitSpherePoint action is deliberately deferred until the closed transform evaluator has a reusable metric-preservation proof; the previous unchecked wrapper was not retained.

Named-fact attribution is human-declared metadata around an explicitly selected typed implication. It is distinguishable from unification and normalization, but is not authenticated provenance or global theorem lookup.

This conservatively reconciles the verified work from #42, #45, #46, and #47. The inherited branch tips and the decisive distant-coordinate commit are recorded in the design note.

[isomorphisms]

Post-merge executable audit: the unified fixture on current default revision 47557b43053c829d4f8aa1581007002b57f9c59f supports a bounded-green conclusion. The compiler-owned edric009 receipt and independent exact R128 oracle pass. The durable staged acceptance record is proposed in ai-ci#64; Idric#62 adds the one missing negative case for applying a transform to a distinct equal-rank named space. Certified sphere action, arbitrary transforms, generic lowering, and numerical algorithm selection remain outside the verified boundary.