merge: resolve conflicts and fix headers

Author: hyperpolymath

.machine_readable/6a2/META.a2ml

@@ -4,7 +4,7 @@
 # META.a2ml — My Lang meta-level information
 [metadata]
 version = "0.1.0"
-last-updated = "2026-06-05"
+last-updated = "2026-06-14"
 
 [project-info]
 license = "MPL-2.0"
@@ -17,8 +17,12 @@ decisions = [
   { id = "ADR-001", date = "2026-06-02", title = "Dual-track QTT mechanisation (Coq + Idris2) for the solo-core", status = "accepted", note = "The solo dialect's affine/linear kernel is mechanised twice — Coq (Prop) and Idris2 (Type) — so the two flagship metatheories track the same shape. Methodology is statements-first: theorems committed as statements, then discharged. Semiring laws proved by exhaustive Refl/reflexivity." },
   { id = "ADR-002", date = "2026-06-05", title = "Echo-types is a first-class type former in the formal kernel", status = "accepted", note = "echo-types is integrated into the type SYSTEM, not only the Rust checker: TEcho type former + MkEcho/Weaken terms + THEcho/THWeaken typing rules + echo reduction rules in the Coq/Idris solo-core. EchoMode = Linear/Affine thin poset (weaken + no-section laws); EchoResidue = proof-layer object pinning the laws behind the Rust Ty::is_assignable_from Echo case (closes slice 3 of docs/design/echo-types-integration.md). Claim line held to R-2026-05-18: Echo is a loss-graded reindexing modality over a thin poset — NOT graded-comonad/universal-property/adjunction." },
   { id = "ADR-003", date = "2026-06-05", title = "Idris splitting rules carry explicit context/quantity fields", status = "accepted", note = "On the Idris track the four context-splitting rules (THApp/THPair/THCase/THLet) carry their split contexts (and the App/Let quantity) as explicit constructor fields. Rationale: Idris2 QTT erases the typing-derivation context indices at runtime, but the closed-context progress inversion (g1+g2=Empty implies both Empty) needs them relevant. The Coq twin leaves them as Prop binders (Prop has no erasure). Documented track divergence; the derivation now records its own split, which is arguably more faithful." },
-  { id = "ADR-004", date = "2026-06-05", title = "Product/elimination form undecided — gates F1.4 preservation", status = "open", note = "Kernel pairs are multiplicative (THPair splits the context) but eliminators are projections (Fst/Snd); that combination is unsound for preservation on open terms. Decision pending between additive (projections), multiplicative tensor (let-pair elim), or both. See issue #93. Preservation (F1.4) is blocked until resolved." },
+  { id = "ADR-004", date = "2026-06-05", title = "Product/elimination form undecided — gates F1.4 preservation", status = "resolved", resolved-date = "2026-06-13", note = "RESOLVED by ADR-007 (both products). Original concern: kernel pairs were multiplicative (split context at intro) but eliminated by projection (Fst/Snd) — neither & nor ⊗, and strictly weaker than both. The resolution is to provide BOTH genuine products. See ADR-007." },
   { id = "ADR-005", date = "2026-06-05", title = "Scope unchanged — no new realignment ANCHOR", status = "accepted", note = "This session (operational semantics, progress, Echo-in-the-typesystem) is progress WITHIN the 2026-01-01 scope-arrest ANCHOR (Solo-first; Rust impl; contain other dialects). It is not a scope realignment, so no new ANCHOR.*.a2ml is issued. Formal mechanisation remains a first-class deliverable consistent with that anchor; proof assistants (Coq/Idris/Agda) are verification tooling, not new compiler host languages." },
+  { id = "ADR-006", date = "2026-06-12", title = "Separated QTT context: type context (tctx) + usage vector (uvec)", status = "accepted", note = "The conflated QTT context (types and quantities together in one Snoc, with ctx_add taking its type annotation from its FIRST argument — so context addition was NOT commutative in the types) is replaced by a SEPARATED representation: a type context tctx (TEmpty/TSnoc) shared verbatim across every premise of a rule, and a usage vector uvec (UEmpty/USnoc) that is the only thing split (uadd) or scaled (uscale). Payoff: uadd is genuinely commutative + associative and uscale distributes (uadd_comm, uadd_assoc, uscale_add in Usage.v), which is exactly the clean algebra the F1.4 substitution lemma needs. has_type : tctx -> uvec -> tm -> ty -> Prop. PRs #102 (Usage.v) + #103 (migration)." },
+  { id = "ADR-007", date = "2026-06-13", title = "Two genuine products: additive & (TWith) and multiplicative ⊗ (TTensor)", status = "accepted", note = "Resolves ADR-004. The additive product & (TWith) introduces under SHARED usage (both components typed under the same D — safe because only one survives elimination) and is eliminated by Fst/Snd projection. The multiplicative product ⊗ (TTensor) introduces by SPLITTING usage (uadd D1 D2) and is eliminated by a let-pair `let (x,y)=e1 in e2` that binds two variables and delivers both components. This replaces the single incoherent product. PRs #103 (&) + #104 (⊗)." },
+  { id = "ADR-008", date = "2026-06-13", title = "Additive-& evaluation is eager (lazy deferred)", status = "accepted", note = "The additive pair With t1 t2 is a value only once BOTH components are values (eager); Fst/Snd project from that value. This is type-safe and, under the current strongly-normalising kernel (no recursion/fixpoint), observationally equivalent to the canonical LAZY & semantics. Switch to lazy & (With always a value; project-then-evaluate) is deferred to when recursion or effects enter the language, at which point lazy becomes required. Flagged, not forgotten." },
+  { id = "ADR-009", date = "2026-06-14", title = "F1.4 preservation via an open-context QTT substitution lemma", status = "accepted", note = "Preservation (Coq) is discharged by a substitution lemma ht_subst that holds for OPEN substituends (not only closed values), because the let-pair (⊗) eliminator substitutes tensor components that are typed in a non-empty context. subst2 u1 u2 t = subst0 u1 (subst0 (shift 0 u2) t) (the shift 0 makes it correct for open u2; identity on closed terms, so closed-program evaluation is unchanged). Theorem preservation + affine_pres are real axiom-free Qed (Print Assumptions closed). PR with d174c06." },
 ]
 
 [development-practices]

.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) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # A2ML 6a2 Directory
 

.machine_readable/contractiles/Adjustfile.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Adjustfile — Drift-tolerance contract for rsr-template-repo
+# Adjustfile — Drift-tolerance contract for my-lang
 # Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # Cumulative-drift catchment: tolerance bands + corrective actions.
@@ -8,65 +8,66 @@
 # Fix with: adjust fix (applies deterministic patches; advisory otherwise)
 
 @abstract:
-Drift tolerances and corrective actions for rsr-template-repo. Unlike
-MUST (hard gate), ADJUST tracks cumulative drift against tolerance bands
-and proposes corrective actions. Advisory — it warns and trends, it does
-not block.
+Drift tolerances and corrective actions for my-lang. Unlike MUST (hard gate),
+ADJUST tracks cumulative drift against tolerance bands and proposes corrective
+actions. Advisory — it warns and trends, it does not block.
 @end
 
-## Template Drift
+## Template-Consumer Drift
 
 ### placeholder-drift
-- description: Template placeholders should be replaced when copied
-- tolerance: 0 placeholder markers in copied repos
-- corrective: Search and replace all {{PLACEHOLDER}} markers
+- description: No unsubstituted template placeholders remain
+- tolerance: 0 {{PLACEHOLDER}} markers anywhere in .machine_readable/
+- corrective: Search and replace all {{PLACEHOLDER}} markers with my-lang values
 - severity: advisory
-- notes: This check only applies to repos that copied from this template
 
-### template-version-drift
-- description: Template version should match RSR spec version
-- tolerance: Template version matches current RSR spec
-- corrective: Update template to match latest RSR spec
+### template-identity-drift
+- description: Contractiles and machine-readable files identify as my-lang, not
+    as the upstream RSR template
+- tolerance: 0 'rsr-template-repo' self-identifiers
+- corrective: Re-author copied template prose to be about my-lang
 - severity: advisory
+- notes: my-lang is a consumer of the RSR template
 
 ## Documentation Drift
 
 ### readme-completeness
-- description: README should document all template features
-- tolerance: README covers all contractiles and directory structure
-- corrective: Update README.adoc with missing sections
+- description: README should document the contractile set and the bust/dust design
+- tolerance: README covers all six verbs and the multi-file bust/dust directories
+- corrective: Update .machine_readable/contractiles/README.adoc
 - severity: advisory
 
-### example-accuracy
-- description: Examples in documentation should match actual template content
-- tolerance: All code examples in docs are accurate
-- corrective: Audit and fix examples in documentation
+### status-doc-currency
+- description: proofs/STATUS.md + 6a2/STATE.a2ml reflect the actual proof state
+- tolerance: Status registry matches the mechanised cores
+- corrective: Refresh STATUS.md / STATE.a2ml after any proof rung lands
 - severity: advisory
 
 ## Structural Drift
 
 ### contractile-sync
-- description: All contractiles should have matching a2ml and ncl implementations
-- tolerance: Every .a2ml has a corresponding .ncl
-- corrective: Generate missing .ncl files from .a2ml
+- description: Singular contractiles have matching a2ml (+ ncl where runners exist)
+- tolerance: Every singular *.a2ml has a corresponding runner where one is expected
+- corrective: Generate missing runner files from the a2ml
 - severity: advisory
 
 ### no-broken-symlinks
-- description: No broken symbolic links in template structure
+- description: No broken symbolic links in the repo structure
 - tolerance: 0 broken symlinks
 - corrective: Run symlink-check script
 - severity: advisory
 
 ## Accessibility Drift
 
 ### adoc-not-md
-- description: Template docs should prefer AsciiDoc
+- description: New prose docs should prefer AsciiDoc (estate convention)
 - tolerance: New prose docs are *.adoc
-- corrective: Convert any new *.md to *.adoc
+- corrective: Convert any new *.md to *.adoc where appropriate
 - severity: advisory
+- notes: Existing *.md (e.g. proofs/STATUS.md) are grandfathered
 
 ### spdx-header-consistency
-- description: All template files have correct SPDX headers
+- description: All source/doc files have correct SPDX headers
 - tolerance: 0 files missing SPDX-License-Identifier
 - corrective: Add SPDX headers to files that need them
 - severity: advisory

.machine_readable/contractiles/Intentfile.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-# Intentfile (A2ML Canonical) — north-star contractile for rsr-template-repo
+# Intentfile (A2ML Canonical) — north-star contractile for my-lang
 # Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # Paired runner: intend.ncl
@@ -10,90 +10,107 @@
 #            become. Two sections share one file because they answer
 #            the same question at different ranges:
 #              [[intents]] — "we WILL do this; track progress"
-#                            status: declared → in_progress → done |
+#                            status: declared -> in_progress -> done |
 #                                    deferred | retired
 #              [[wishes]]  — "we WISH this were true; revisit later"
-#                            status: declared → in_progress → achieved |
+#                            status: declared -> in_progress -> achieved |
 #                                    abandoned
 #                            grouped by horizon: near / mid / far.
 #            Non-gating — this is a report, not a gate. See the `must`
 #            contractile for hard gates.
 
 @abstract:
-North-star contractile for rsr-template-repo. This repository is the
-canonical template for Rhodium Standard Repository compliance. It provides
-the scaffold that all hyperpolymath repos should copy and customize.
+North-star contractile for my-lang: a multi-dialect programming language with a
+Quantitative Type Theory (QTT) semantic core, whose affine Solo kernel is
+mechanised twice (Coq + Idris2) as a first-class deliverable alongside the Rust
+compiler. Echo-types are integrated into the formal type system.
 @end
 
 ## Purpose
 
-The rsr-template-repo serves as the master template for all hyperpolymath
-repositories. It contains the complete set of contractile files, machine-readable
-specifications, and governance documentation that define the Rhodium Standard.
-
-Every new repository in the hyperpolymath estate should be initialized by
-copying this template and substituting the placeholder values with
-repo-specific content.
+my-lang explores a QTT-cored language with THREE NESTED dialects —
+Solo (affine, single-agent) c Duet (session-typed, two-party) c Ensemble
+(multi-agent) — plus "Me", an on-the-fly agent-generated PROJECTION over the
+dialect hierarchy (NOT a fourth dialect). Formal verification of the kernel
+(progress + preservation over the separated QTT context, both products, and the
+Echo modality) is a first-class deliverable: the mechanised solo-core leads the
+Rust implementation and becomes the spec the checker must satisfy.
 
 ## Anti-Purpose
 
-This repository is NOT:
-- A general-purpose project scaffold for external use (hyperpolymath-only)
-- A replacement for per-repo customization (all files must be bespoke)
-- A static template that never changes (evolves with RSR spec)
-- A runtime library or framework (build-time only)
+my-lang is NOT:
+- The RSR template repository (it is a CONSUMER of that template)
+- A single-dialect language (the dialect hierarchy is the point)
+- A dependently-typed language (Echo is the non-dependent approximation)
+- A finished compiler (the mechanised core currently leads the implementation)
 
 ## If In Doubt
 
 If you are unsure whether a change is in scope, ask. Sensitive areas:
-- .machine_readable/ contractile definitions
-- RSR specification files
-- Governance templates
-- License policy documents
+- proofs/verification/ mechanised cores (Coq + Idris2 solo-core)
+- .machine_readable/ contractile + 6a2 definitions
+- the scope-arrest ANCHOR and AUTHORITY_STACK
+- governance / licence policy documents
 
 ## Committed Next-Actions
 
-### repo-initialization
-- description: Provide just copy-and-substitute template for new repos
-- probe: test -f scripts/init-repo.sh
-- status: done
-- notes: Run with source scripts/init-repo.sh <new-repo-name>
+### proof-ci
+- description: Add a CI leg that runs coqc (solo-core) + idris2 --build so the
+    proofs are machine-checked, not only locally-checked (closes proof-ci=absent)
+- probe: test -f .github/workflows/proofs.yml
+- status: declared
+- notes: Mirror echo-types' agda.yml pattern; the root F5 gap
 
-### contractile-completeness
-- description: Every RSR contractile has an a2ml and ncl implementation
-- probe: ls .machine_readable/contractiles/*.a2ml | wc -l | grep -q "^6$"
+### idris-track-preservation
+- description: Discharge ?todo_preservation on the Idris2 twin (Coq F1.4 is done)
+- probe: test -z "$(grep -r '?todo_preservation' proofs/verification/idris 2>/dev/null)"
 - status: in_progress
-- notes: Currently 6 contractile verbs: intend, must, trust, adjust, bust, dust
+- notes: Open-context subst2 generalisation from the Coq track is the template
 
-### automation-scripts
-- description: All repetitive tasks have just recipes
-- probe: grep -c "^# " Justfile | grep -q "^[6-9][0-9]*$"
-- status: in_progress
+### four-point-semiring
+- description: Extend the three-point QTT semiring to four-point affine (add ?)
+- status: declared
+- notes: F1.2; matches proofs/solo/affine-types/formal-system.md
+
+### echo-parser-syntax
+- description: Surface syntax for Echo<A => B> in the solo dialect (slice 2)
+- status: declared
 
 ## Wishes
 
 ### Near Horizon
 
-#### cross-repo-validation
-- description: Tooling to validate all repos against RSR spec
-- horizon: near
-- status: declared
-
-#### automated-substitution
-- description: Script to automate repo-specific substitution in template
+#### dialect-parity
+- description: Duet + Ensemble mechanised cores reach the Solo core's rigour
 - horizon: near
 - status: declared
 
 ### Mid Horizon
 
-#### formal-verification
-- description: Idris2 proofs for all critical contractile invariants
+#### effects-and-memory-metatheory
+- description: Mechanised effect-row + ownership/borrowing soundness (F2/F3)
 - horizon: mid
 - status: declared
 
 ### Far Horizon
 
-#### ecosystem-visualization
-- description: Interactive graph of all hyperpolymath repos and dependencies
+#### me-projection-runtime
+- description: The "Me" projector renders dialect-hierarchy projections on the fly
 - horizon: far
 - status: declared
+- notes: Specified in tentacles-agentic-syllabus/me/README.adoc (out-of-repo)
+
+## Structure Note
+
+The six contractile verbs are intend / must / trust / adjust / bust / dust.
+intend, must, trust, adjust are SINGULAR (one flat *.a2ml each). bust and dust
+are MULTI-FILE by design and live as directories: one `bust` entry per
+failure-mode / issue, one `dust` entry per cleanup intention (e.g. uninstall,
+detach-a-component-as-plugin, larger teardown operations).
+
+### contractile-completeness
+- description: Four singular verbs present as flat files; bust/ and dust/ present
+    as (multi-file) directories
+- probe: test -f .machine_readable/contractiles/Intentfile.a2ml && test -f .machine_readable/contractiles/Mustfile.a2ml && test -f .machine_readable/contractiles/Trustfile.a2ml && test -f .machine_readable/contractiles/Adjustfile.a2ml && test -d .machine_readable/contractiles/bust && test -d .machine_readable/contractiles/dust
+- status: done
+- notes: Six verbs; bust/dust are directories (see Structure Note)