QTT solo-core mechanisation: F1.4 + R2–R5 + M1 + S1–S3c + E4 + contractile overhaul (#111)

## Summary

Large mechanisation milestone — the dev branch accumulates all proof
work since v0.3.0 (post-PR #110).

### Coq solo-core advances (Coq 8.18.0, `−R . SoloCore`, axiom-free
throughout)

**F1.4 — Separated QTT context + both products + preservation
(complete)**
- Separated `tctx` (types) + `uvec` (quantities); `uadd` genuinely
commutative/associative
- Additive `&` (`TWith`, shared D, `Fst`/`Snd`) + multiplicative `⊗`
(`TTensor`, split D, `LetPair`)
- `ht_subst` open-context substitution lemma; `Theorem preservation :
Preservation. Qed.`
- `Theorem progress : Preservation. Qed.` — both axiom-free (`Print
Assumptions` closed)

**R2–R5 — Semiring functorisation + affine sub-usage + decidability**
- R2: parametric soundness functor over any QTT semiring (tropical
min-plus instance)
- R3: affine sub-usage layer (`affine_pres` distinct)
- R5: verified usage-walk checker ≡ static context-splitting
(`check_sound`, `check_complete`, `check_correct`)
- R5b: decidability of the affine judgement (`aff_type_dec`)

**M1 — Me dialect + elaboration into Solo (mechanised translation)**
- M1.0: `me_tm` AST + `translate : me_tm → solo_tm`
- M1.1: universal elaboration adequacy (Visual Soundness, axiom-free)
- M1.1b: universal linear-use `me_wt` spanning all `me_tm`; `MeIf`
faithful

**S1–S3c — Ensemble session-π core (n-party, axiom-free)**
- S1.0: session-typed π-calculus (`SessionPi.v`); duality involution;
well-typed ping-pong
- S1.1a/b: communication-redex SR + full closed-system SR over
`(νc)(P∣Q)`
- S1.2: session fidelity + progress/deadlock-freedom
- S1.3: n-ary labelled choice + equi-recursive `μ` type-layer +
structural congruence preserves typing
- S2: Duet by projection (axis-2 STRUCTURE; `proj_g` + `merge`)
- S2.2: global choice + recursion by projection
- S3a: n-party projection totality (first n≥3 theorem)
- S3b: static n-party configuration
- S3c.0–S3c.3: full label-union merge (`umerge`) + union-projection +
n-ary located semantics + head-coupled message subject reduction (first
earned n-party safety)

**E4 — Echo-types residue-measure SEAM (Coq mirror, axiom-free)**
- Coq mirror of the echo-types residue SEAM; `EchoMode` (Linear/Affine);
`EchoResidue`

### Contractile overhaul

The RSR-template-copied `Bustfile.a2ml` / `Dustfile.a2ml` both
incorrectly described my-lang as "the canonical template for RSR
compliance". my-lang is a **consumer** of the RSR template.

Replaced with properly-scoped per-intent named files:
- `bust/proof-ci-gate-absent.a2ml` — F5 gap (proofs.yml absent;
axiom-regression mode)
- `bust/idris2-parity-lag.a2ml` — Idris2 twin lags Coq on F1.4
(`?todo_preservation`, issue #108)
- `dust/uninstall-coq-toolchain.a2ml` — clean Coq toolchain removal
procedure
- `dust/detach-echo-types-plugin.a2ml` — extract
`TEcho`/`MkEcho`/`Weaken` as plugin crate

`bust/` and `dust/` are **multi-file by design** — one bust entry per
failure-mode, one dust entry per cleanup intention.

## Test plan

- [ ] `coq_makefile -f _CoqProject -o CoqMakefile && make -f
CoqMakefile` exits 0 in `proofs/verification/coq/solo-core/`
- [ ] `Print Assumptions preservation.` → "Closed under the global
context" for all headline theorems
- [ ] `idris2 --build solo-core.ipkg` exits 0 (Idris2 parity tracked
separately, issue #108)
- [ ] `cargo test` exits 0
- [ ] `.machine_readable/contractiles/bust/*.a2ml` and `dust/*.a2ml`
each have ≥1 file (Mustfile check)
- [ ] No `Admitted` / stray `Axiom` in the Coq source

https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV

---
_Generated by [Claude
Code](https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV)_

Author: hyperpolymath

.github/workflows/proofs.yml

@@ -70,4 +70,5 @@ CoqMakefile.conf
 *.vos
 *.glob
 .*.aux
+.*.d
 .lia.cache

.gitignore

@@ -1,4 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # A2ML 6a2 Directory
 

.machine_readable/6a2/README.adoc

@@ -1,4 +1,5 @@
 // SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = Contractiles (my-lang)
 :toc:

.machine_readable/6a2/STATE.a2ml

@@ -0,0 +1,45 @@
+# SPDX-License-Identifier: MPL-2.0
+# bust/idris2-parity-lag.a2ml — Failure mode: Idris2 twin lags Coq canonical
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Verb: bust
+# Scope: my-lang Idris2 mechanised solo-core (twin of the canonical Coq core)
+# Failure mode: Idris2 ?todo_preservation open while Coq F1.4 is closed
+
+@abstract:
+The Idris2 twin of the mechanised solo-core is behind the Coq canonical.
+F1.4 preservation is discharged in Coq (axiom-free, PR #104) but
+?todo_preservation remains open on the Idris2 track (issue #108).
+This is a parity-lag failure mode: the spec the Rust checker must
+satisfy is split across two mechanisations that are not in sync.
+@end
+
+## Failure Mode
+
+### idris2-preservation-open
+- class: parity_lag
+- description: ?todo_preservation in proofs/verification/idris/ is not discharged.
+    The Idris2 twin cannot independently verify F1.4 preservation.
+- detection: "grep -r '?todo_preservation' proofs/verification/idris/ 2>/dev/null | grep -c ."
+- recovery_probe: "test -z \"$(grep -r '?todo_preservation' proofs/verification/idris/ 2>/dev/null)\""
+- recovery_path: >
+    Discharge ?todo_preservation on the Idris2 track following the Coq template.
+    Key: open-context substitution generalisation (ht_subst analogue in Idris2).
+    Subst2 is subst0 u1 (subst0 (shift 0 u2) t) — carry the shifted-substituend
+    lemma from the Coq ContextProps.v track.
+- expected_recovery_time_seconds: 14400
+- escalation: File GitHub issue (already filed as #108); track as in_progress in Intentfile
+- status: declared
+- notes: Coq F1.4 is done. The open-context subst2 generalisation is the template.
+
+### idris2-build-broken
+- class: build_integrity
+- description: idris2 --build for the solo-core package fails; the Idris2
+    mechanised core does not compile.
+- detection: "cd proofs/verification/idris && idris2 --build solo-core.ipkg 2>&1 | grep -q 'error'"
+- recovery_path: >
+    Run idris2 --build; fix type errors.  Usually triggered by upstream
+    Idris2 API changes.  Pin the Idris2 version in CI to 0.7.0 until the
+    solo-core is updated.
+- expected_recovery_time_seconds: 1800
+- status: declared

.machine_readable/contractiles/README.adoc

@@ -0,0 +1,42 @@
+# SPDX-License-Identifier: MPL-2.0
+# bust/proof-ci-gate-absent.a2ml — Failure mode: proof CI not running
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Verb: bust
+# Scope: my-lang (QTT multi-dialect language with mechanised Coq + Idris2 solo-core)
+# Failure mode: F5 gap — the proof CI leg is absent or disabled
+
+@abstract:
+The mechanised solo-core proofs (Coq + Idris2) are not machine-checked in CI.
+This is the F5 gap: progress/preservation/axiom-freedom are locally verified
+but not enforced on every push. A regression that slips an `Admitted` into the
+substitution chain would pass CI silently.
+@end
+
+## Failure Mode
+
+### proof-ci-gate-absent
+- class: ci_gap
+- description: .github/workflows/proofs.yml missing or disabled; Coq + Idris2 proofs
+    are not machine-checked on push. Any `Admitted` or axiom regression
+    reaches main silently.
+- injection_probe: "mv .github/workflows/proofs.yml /tmp/proofs.yml.bak"
+- recovery_probe: "mv /tmp/proofs.yml.bak .github/workflows/proofs.yml"
+- detection: "test -f .github/workflows/proofs.yml && grep -q 'coqc\|coq_makefile' .github/workflows/proofs.yml"
+- recovery_path: Restore proofs.yml; see Intentfile.a2ml probe 'proof-ci'
+- expected_recovery_time_seconds: 300
+- status: declared
+- notes: F5 intent recorded in Intentfile.a2ml; mirrors echo-types' agda.yml pattern
+
+### axiom-regression
+- class: proof_integrity
+- description: An `Admitted`, `admit`, or stray `Axiom` enters the substitution /
+    preservation dependency cone without CI catching it.
+- detection: "coqtop -R proofs/verification/coq/solo-core SoloCore -e 'Require Import SoloCore. Print Assumptions preservation.' 2>/dev/null | grep -q 'Closed under the global context'"
+- recovery_path: >
+    Identify the regression via `Print Assumptions preservation.` in coqtop.
+    Remove the admitted term; discharge the obligation or file a Bustfile entry
+    for the open proof obligation.
+- expected_recovery_time_seconds: 3600
+- status: declared
+- notes: CI currently checks this via proofs.yml axiom-free steps for all headline theorems

.machine_readable/contractiles/bust/Bustfile.a2ml

@@ -0,0 +1,69 @@
+# SPDX-License-Identifier: MPL-2.0
+# dust/detach-echo-types-plugin.a2ml — Cleanup intention: detach echo-types integration
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Verb: dust
+# Scope: my-lang echo-types integration in the type system
+# Cleanup intention: detach the echo-types formal integration as a standalone plugin
+#   if the project adopts a plugin architecture or needs to ship echo-types separately
+
+@abstract:
+How to cleanly detach the echo-types type-system integration from my-lang's
+core type checker, exposing it as a plugin/optional extension rather than a
+built-in. This is advisory — echo-types are currently integrated into the
+type system as TEcho/MkEcho/Weaken and are not optional. Detachment would
+be a significant architectural change requiring a clear extension boundary.
+@end
+
+## Cleanup Intention
+
+### scope
+- description: Separate echo-types from the core QTT type system into a plugin layer
+- trigger: Plugin architecture adoption; shipping echo-types as a standalone crate
+- authority: Requires ADR update in META.a2ml; review with echo-types maintainer
+
+## Steps
+
+### 1-define-extension-boundary
+- description: Identify the minimal interface for echo-types integration
+- notes: >
+    Current integration points in Typing.v / solo-core:
+    - TEcho former type constructor
+    - MkEcho / Weaken term constructors
+    - T_Echo / T_Weaken typing rules
+    - EchoMode (Linear/Affine) thin poset
+    - EchoResidue (weakened representation)
+    A plugin boundary must expose all five without coupling the core to
+    the echo-types Coq/Agda formalisations.
+
+### 2-extract-echo-module
+- description: Move TEcho/MkEcho/Weaken/T_Echo/T_Weaken into a separate Coq module
+- run: "cp proofs/verification/coq/solo-core/Typing.v /tmp/Typing.v.bak"
+- corrective: >
+    Create proofs/verification/coq/solo-core/EchoIntegration.v with the echo
+    constructors; update Typing.v to Import EchoIntegration.  This is the
+    boundary-extraction slice.
+
+### 3-extract-echo-crate
+- description: Extract echo-types Rust integration into a separate crate
+- corrective: >
+    Create crates/my-lang-echo/ with the TEcho representation; make
+    crates/my-lang/ depend on it optionally via a feature flag.
+    Update Cargo.toml: [features] echo = ["my-lang-echo"].
+
+### 4-update-checker
+- description: Gate TEcho handling in the type checker behind the echo feature flag
+- corrective: >
+    In crates/my-lang/src/checker.rs: wrap TEcho/MkEcho arms in
+    #[cfg(feature = "echo")] or return a FeatureGated error.
+
+### 5-update-6a2-state
+- description: Update STATE.a2ml to reflect echo-types as plugin, not built-in
+- corrective: >
+    In 6a2/STATE.a2ml: update echo_integration_status from 'built_in' to 'plugin'.
+    Add an ADR in META.a2ml documenting the boundary decision.
+
+## Completion Criteria
+- run: "cargo build --no-default-features 2>&1 | grep -v echo | grep -c error || true"
+- notes: Build without echo feature should succeed (zero non-echo errors)
+- severity: advisory