Compile higher-math constraints and typed contraction against Edric

[isomorphisms]

Scope

Turn the research branch into a real compiler-checked experiment without broadening the semantic claims beyond what these finite models establish.

Verified contraction boundary

The checked interface remains space-indexed:

contract : Covector space -> Vector space -> Integer

The receipt now covers:

• contraction only when both arguments share the same named space;
• the exact PlaneSpace / ThreeSpace rejection diagnostic;
• rejection of PlaneSpace / ImagePlaneSpace despite their equal coordinate counts, pinning the constraint to nominal space identity rather than rank;
• rejection of vector-vector contraction in the absence of an implicit metric or vector-to-covector conversion;
• concrete evaluation, additivity, and scalar compatibility in both arguments.

These checks do not introduce or claim a general Group/Module/Tensor hierarchy.

Verified presheaf tensor restriction boundary

The example is explicitly a finite formal model of elementary-generator pairs for
Section(U) tensor Section(U) over Whole, Patch, and Point.

The compiler checks:

• the named componentwise restriction law;
• restriction identity definitionally, including for an opaque tensor value;
• every composable restriction case;
• the focused theorem module with unbound implicits disabled, preventing accidental auto-bound witnesses.

This is not a balanced tensor-product quotient, arbitrary presheaves F and G, sheafification, or a function-extensionality theorem.

Receipt hardening

• Preserve the .idric extension when staging fixtures so the filename-scoped → syntax is actually exercised.
• Express expected type failures as compiler-native failing blocks.
• Compile the focused presheaf theorem module as part of the test.
• Run through ./edric test --only idris2/basic/edric008 with the bootstrapped Chez executable pinned through CHEZ.
• Check out and assert the exact PR source-head SHA in Actions.
• Run the invariant on every PR targeting Idriç and every default-branch push, without duplicate feature-branch push receipts.
• Remove the obsolete shell-driven Bad.idr probe, whose stdout/stderr assumptions did not reliably observe the compiler diagnostic.

Exact-head receipt

Head: c2e5945e209cbf9ab055e3c127c4b981313242fc

• Edric higher-math smoke — run #9: passed
  • exact source-head assertion passed;
  • bootstrap passed;
  • idris2/basic/edric008: success;
  • 1/1 tests successful.
• Edric wrapper — run #63: passed
  • verifies the private Scheme path, exact CHEZ pin, bootstrap delegation, and focused test delegation.

The executable receipt prints:

shared-space contraction and mismatch diagnostics: checked
no implicit vector-to-covector conversion: checked
presheaf tensor restriction identity/composition: checked

Still deferred / research-only

Actual compiler lexer/elaborator support for the proposed glyph syntax, compiler IR/planning integration, theorem-aware inference, a general tensor-product construction, and sheafification remain unimplemented and are not claimed by this PR.

Relation to the geometry stack

This PR is independent of the #44 → #45 → #47 stack. That stack models rank-indexed Euclidean coordinate vectors with a direct dot product; this PR models nominally named spaces and permits contraction only between Covector space and Vector space, with no implicit metric. Both use tests/idris2/basic/edric008, so their fixture collision and mathematical disagreement must be resolved deliberately rather than by selecting the branch with more code.

[isomorphisms]

Classification: SUPERSEDED by #51.

#51 retained the named-space distinction, separate vector/covector representations, contraction machinery, and presheaf identity/composition laws, while reconciling them with the competing Euclidean geometry line.

No unique implementation from this PR remains pending outside the unified model in #51. This PR remains the historical record of the named-space design.