proofs(agda): the wager experiment, stages 5 to 7 (T6, T7, the cross-check) and the final verdict

CHANGELOG.adoc

@@ -21,7 +21,7 @@ open proof obligation.
 and the AFFIRMATION honesty snapshot with the systemet identity and an
 honest status (theory specified; proofs OPEN; no compiler here).
 * Added the wager experiment for coercions and roles in Cubical Agda
-(`+verification/proofs/agda/Wager/+`, stages 0 to 4), with an `+agda+` job
+(`+verification/proofs/agda/Wager/+`, stages 0 to 7), with an `+agda+` job
 in the proofs workflow. The experiment claims no ET obligation.
 
 ==== Changed

docs/status/PROOF-STATUS.adoc

@@ -13,7 +13,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees.
 // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh.
 // Do not edit by hand without changing the MANIFEST accordingly.
 // gate:lean4 gated=20 quarantined=0
-// gate:agda gated=64 quarantined=0
+// gate:agda gated=79 quarantined=0
 
 == Summary
 
@@ -24,7 +24,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees.
 | ET obligations (DOM — the theory itself) | 15 | 2 | 2 | 11
 | MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | —
 | MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | —
-| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation) | 1 | - | in progress | -
+| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation; stages 0 to 7 are done; 2 decisions are with the owner) | 1 | 1 | - | -
 |===
 
 The Done/In-progress claims above are scoped to the *mechanized core
@@ -158,9 +158,40 @@ no file uses coinduction. One warning class is silenced
   newtype parameter is the least grade that target kinding accepts
 | *Proven*
 
-| 5 to 7
-| T6, T7 of the experiment
-| not attempted
+| 5
+| `Wager.Proofs.t6`, `t6-conversion`, `t6-no-term` : for each nominal
+  coercion of the source fragment, the two translated types have one normal
+  form; the coercion becomes conversion and no term remains
+| *Proven*. The converse is false for one checked pair of types
+
+| 6
+| T7 of the experiment (local equality assumptions), in 2 parts.
+  Part 1, a separation. `Wager.Proofs.t7-separation` : for each closed
+  instance of one GADT program of a source calculus with local equality
+  assumptions, no typed closed target term has the erasure of the program
+  together with a type that has the erased type of the source type.
+  Part 2, an identity type at the grade `0`, as a family of base constants
+  of a signature. Equality evidence is a term. `Wager.Proofs.t7-erasure`,
+  `t7-canonicity`, `t7-intro`, `t7-grade`, `t7-assumption`,
+  `t7-conservative` : the erasure of the proofs in casts is sound; closed
+  evidence exists exactly for convertible types; a local equality
+  assumption is a variable at the grade `0`
+| Part 1 *Proven*. It excludes a translation that keeps the erased type
+  and the erased term, and no other translation.
+  Part 2 *Proven* for a signature that has an identity family (one such
+  signature is built). The extension has 1 new rule and 1 new term former.
+  The owner decides if it is inside the wager
+
+| 7
+| The optional univalent cross-check. `Wager.Proofs.coercion-denotes-transport`,
+  `coercion-denotes-transport-back`, `coerce-function-is-transport` : in a
+  realisability model of the target types in the cubical universe, where a
+  newtype instance is a wrapper that is equivalent to its content, the
+  translation of each representational coercion denotes transport along a
+  path made with `ua`
+| *Proven*, for each source signature that passes the role check. The
+  denotation is by realisers: the development has no denotation of each
+  typed term
 |===
 
 == Mechanization slots

verification/proofs/agda/MANIFEST

@@ -65,3 +65,18 @@ verification/proofs/agda|Wager/Trans/Simulation.agda|gated|Stage 4 (T3, T5): an
 verification/proofs/agda|Wager/Trans/RoleCorrespondence.agda|gated|Stage 4: the inferred source role is the least grade that target kinding accepts; the target signature is valid
 verification/proofs/agda|Wager/Trans/TwoStateProofs.agda|gated|Stage 4: the tagged signature has no translation with two-state tropes (checked counterexample)
 verification/proofs/agda|Wager/Examples/Stage4.agda|gated|Stage 4: accepted and rejected closed examples
+verification/proofs/agda|Wager/Examples/Stage5.agda|gated|Stage 5 (T6): accepted and rejected closed examples; the converse of T6 is false for the row scheme
+verification/proofs/agda|Wager/L2/Erasure.agda|gated|Stage 6 (lemma): a typed target term erases to a simply typed term, for each signature and each grade algebra
+verification/proofs/agda|Wager/Local/Source.agda|gated|Stage 6: the source calculus with local equality assumptions (types, equalities, terms, erasure)
+verification/proofs/agda|Wager/Local/Gadt.agda|gated|Stage 6: the GADT program of the separation (definitions only)
+verification/proofs/agda|Wager/Local/Separation.agda|gated|Stage 6 (T7, the separation): no typed target term has the erasure and the erased type of the GADT program
+verification/proofs/agda|Wager/Examples/Stage6.agda|gated|Stage 6 (T7, the separation): accepted and rejected closed examples
+verification/proofs/agda|Wager/Identity/Family.agda|gated|Stage 6, part 2: the identity type as a family of base constants of a signature (definitions only)
+verification/proofs/agda|Wager/Identity/Term.agda|gated|Stage 6, part 2: the terms of the target with the cast, and the two erasures (definitions only)
+verification/proofs/agda|Wager/Identity/Typing.agda|gated|Stage 6, part 2: the target judgement with the rule t-cast, which uses the evidence at the grade 0 (definitions only)
+verification/proofs/agda|Wager/Identity/Soundness.agda|gated|Stage 6, part 2 (T7, the identity type): the erasure of proofs is sound for each signature with an identity family and each set of grade operations; canonicity; the grade lemma needs the laws
+verification/proofs/agda|Wager/Identity/Instance.agda|gated|Stage 6, part 2: one signature that has an identity family (the record is not empty)
+verification/proofs/agda|Wager/Examples/Stage6Identity.agda|gated|Stage 6, part 2 (T7, the identity type): accepted and rejected closed examples
+verification/proofs/agda|Wager/Univalent/Model.agda|gated|Stage 7 (optional): the model of target types in the cubical universe, realisers, and the path of a coercion (definitions only)
+verification/proofs/agda|Wager/Univalent/CrossCheck.agda|gated|Stage 7 (optional): the translation of a representational coercion denotes transport along its path, for each source signature, state scheme, grade algebra and interpretation of the base constants
+verification/proofs/agda|Wager/Examples/Stage7.agda|gated|Stage 7 (optional): accepted and rejected closed examples