planner/VCL handle 6 of the octad's 8 modalities (Provenance, Spatial unscheduled)

[hyperpolymath]

The octad has eight modalities. The planner and the VCL type checker handle
six. verisim-provenance and verisim-spatial are full, tested crates that
the planner cannot schedule and the type checker does not know about.

Ruled 2026-07-28: keep 6 for now and track the gap here, rather than widen
the enums as a drive-by. Two reasons, and the second is the one that matters.

Where the 6 is

• rust-core/verisim-planner/src/lib.rs — Modality has six constructors
  (Graph, Vector, Tensor, Semantic, Document, Temporal) and Modality::ALL is
  [Modality; 6]. execution_priority covers only those six.
• src/vcl/VCLTypeChecker.res:60 — availableModalities lists the same six,
  while VCLTypes.res:18-26 defines eight (adding ProvenanceModality and
  SpatialModality).
• formal/Planner.v — modality is now an Inductive with six constructors,
  deliberately mirroring the Rust rather than the octad (see feat(formal): discharge optimize_is_permutation — axiom to theorem, in both modules #206). A model that
  covered eight would stop describing the code it validates.

Why this is not a one-line fix

availableModalities is never read. It appears exactly twice in
src/vcl/*.res — its declaration at :43 and its initialiser at :60. Nothing
consumes it. So adding Provenance and Spatial to that list is correct,
costless, and changes no behaviour whatsoever. Shipping it as "fixed the
six-modality bug" would be an overclaim — the field would still be dead, just
dead with eight entries instead of six.

The honest fix is two parts:

1. Add the two constructors, and
2. Either consume the field — reject a proposition or epistemic request naming
   a modality that is not available — or delete it as dead weight.

Until (2) is decided, (1) is cosmetic.

Scope when this is picked up

• Decide: does availableModalities become load-bearing, or get deleted?
• Modality enum + ALL + execution_priority for Provenance and Spatial
  (the priority values are a real decision — Semantic is 90 because ZKP is
  expensive; where do provenance-chain walks and R-tree lookups sit?)
• formal/Planner.v modality Inductive and execution_priority follow the
  Rust, in the same change — they are a mirror, and a silent divergence
  there is worse than the gap itself
• VCLTypeChecker.res + VCLTypes.res alignment
• Cost model paths for both new modalities

Related

• feat(formal): discharge optimize_is_permutation — axiom to theorem, in both modules #206 discharged optimize_is_permutation and mirrors the Rust's six; the
  header records why.
• The same "model drawn around the gap" pattern produced fix(planner): carry projections and early_limit into the physical plan #207 — the Coq node
  abstraction omitted exactly the two PlanNode fields the optimizer was
  dropping. Worth checking whether the missing two modalities hide anything
  similar.