L11: decide graded necessity, spec QTT grade propagation — and fix Modal.idr, which had never compiled

[hyperpolymath]

Closes MOTIVATION.adoc open items 1 (semantics) and 2 (QTT integration).
Then, installing Idris2 and actually running it turned up rather more than that.

TL;DR

Semantics	Decided: neither S4 nor contextual — graded necessity □_r A
QTT integration	Specified — split=+, comult=·, drop=0, unbox gated on 1 ⊑ r
Biggest finding	Modal.idr had never compiled. The comonad laws were verified by nothing
Root cause	Idris2 was never installed here, and CI doesn't gate research/
Second finding	dup pins r = ω — L11 currently adds nothing over L10 (machine-checked)
Third finding	TropicalKleene.idr is also broken (recorded, not fixed here)

1. Semantics — decided: neither

The question ("S4 vs contextual?") was malformed. The two refine □ along
different axes — contextual ([Ψ]A) refines which variables the box may capture;
graded (□_r A) refines how many times its content may be used. They are orthogonal
(one could have [Ψ]_r A), so the question had no answer as posed. L11 exists to
discipline usage, so it takes the quantity axis. S4 is not lost — it is the r = ω
instance. Rationale in SEMANTICS-DECISION.adoc; CMTT assessment in
reading-notes/contextual-modal-types.adoc.

Strict S4 was never really on the table anyway: openPool captures the ordinary variable
uri, so the sketch's own worked example is ill-typed under it. mkBox : a -> Box a had
no promotion rule at all — "S4" was a label on an unruled constructor.

2. QTT integration — specified

QTT-INTEGRATION.adoc: promotion scales the context (r · Γ); unbox extracts at grade
1, admissible iff 1 ⊑ r; dup → split over +; comult over ·; drop at 0.
Resolves the informal "grade of unbox should be ≤ grade of the enclosing context" into
an actual side condition.

3. The big one: Modal.idr had never compiled

Error: While processing type of comonadLaw1. Ambiguous elaboration.
    Modal.dup b
    Prelude.dup b
Error: No type declaration for Modal.comonadLaw1.

Idris2 0.7.0's Prelude exports dup : a -> (a, a). Every signature mentioning dup
failed to elaborate, so comonadLaw1/comonadLaw2 had no type declarations and were
verified by nothing — while the header, the checklist, and STATE.a2ml all recorded them
as proved, believe_me-free, at 100%.

Pre-existing, not from this branch: origin/main's copy fails identically.

Root cause: Idris2 was never installed in this estate. IDRIS2_PREFIX and PACK_DIR
were exported and pack/bin was on PATH, but the pack tree did not exist — so
idris2 --check had never once been runnable locally. CI gates only
a-sounder-constitution/, not research/. An unrunnable proof gate produces confident
false records.

Fixed with %hide Prelude.dup. Modal.idr now checks clean, exit 0 — the laws are proved
for the first time.

4. dup pins the grade to ω — machine-checked

DupForcesOmega.idr (exit 0):

dupForcesOmega : (r : Multiplicity) -> plus r r = r -> Either (r = Zero) (r = Many)
dupForcesOmega Zero Refl = Left Refl
dupForcesOmega One  Refl impossible
dupForcesOmega Many Refl = Right Refl

The One case is impossible: plus One One reduces to Many, so the premise would
need Refl : Many = One. That one unwritable clause is the whole defect. Since r = 0 is
erased, every useful dup pins r = ω — Box a is isomorphic to an L10 value at
multiplicity ω, so L11 currently adds nothing over L10. Exactly what MOTIVATION predicted
in prose; now a proof.

The file also supplies the plus/mult tables Multiplicity never had — it is a bare
enumeration despite its section being titled "semiring". That absence is why the defect
survived: with no + in scope, r + r = r was never a question anyone could ask.

The clash was never a coincidence. Prelude.dup is unrestricted duplication, and at
r = ω the box's dup is Prelude.dup up to the MkBox wrapper. The compiler had
been pointing at the defect the entire time.

5. Second broken proof (recorded, not fixed)

research/tropical/TropicalKleene.idr also fails (exit 1):

costMatAddZeroL m1 m2 i h =
  rewrite h                    -- needs `rewrite h in ...`
  exact latAddZeroL (m2 i i)   -- `exact` is not Idris2 term syntax at all

It uses syntax that has never existed in Idris2 — it cannot ever have been run. Needs
its own PR; there may be more behind the first parse failure.

Proof sweep (idris2 0.7.0, recorded in STATE maintenance-status)

PASS  research/level-candidates/L11-modal-box/Modal.idr        (after this fix)
PASS  research/level-candidates/L11-modal-box/DupForcesOmega.idr
PASS  a-sounder-constitution/formal/Constitution.idr           (the CI-gated one)
FAIL  research/tropical/TropicalKleene.idr                     (pre-existing)

Do not conflate the two grades

Grades here are usage grades over {0,1,ω} — not the tropical disclosure grades
of epistemic-types' EchoBridge/Echo (the RMR/RMO axis). Both are graded comonads: same
shape, different semiring, different theorem. Fusing them would identify "used twice" with
"leaked twice". QTT-INTEGRATION.adoc §1.

Graduation

2 of 6 done (one only as of today), 1 spec'd, 3 not started, plus the rewrite this
surfaced. Not close. First graduated artefact promoted to typell stays at 0%;
STATE 25% → 30%, open-failures 0 → 1.

Recommended next, in order

1. Extend the Idris2 CI gate to research/ — both modules check in <1s now. Until it
   exists, no research milestone in STATE.a2ml is trustworthy.
2. Audit other estate repos recording Idris2 milestones for the same unrunnable-gate
   failure mode.
3. Fix TropicalKleene.idr (own PR).
4. Rewrite Modal.idr to graded Box.

🤖 Generated with Claude Code

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud