feat(formal): F-5 — render_ty per-face type renaming is injective (no collision)

Mechanizes F-5 (docs/PROOF-NEEDS.adoc): lib/face.ml's render_ty rewrites a fixed
type-name vocabulary per face (Unit, Bool, Option[_]); F-5 asks whether that
renaming ever collapses two distinct canonical types onto one displayed string —
pointedly, Js renders Unit as "null" and Option[T] as "T | null", sharing the
"null" lexeme.

F5_RenderFaithful.v models the canonical-type vocabulary (cty), the displayed
lexemes (name, distinct constructors), and the rendered form (rty), then mirrors
render_ty as render : face -> cty -> rty. Faithful to two OCaml details: Unit/Bool
are special-cased only at the whole-type level, and Option's inner is rendered
canonically (the global_replace captures the canonical substring), so e.g. Js
Option[Option[Int]] => "Option[Int] | null".

Theorems (axiom-free): canon_inj; render_inj (every face's renaming injective —
the non-collapse guarantee); js_no_collapse / cafe_no_collapse / option_never_atom
(Unit and Option never read as one type despite the shared null/? lexeme).

Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc. PROOF-NEEDS.adoc:
F-5 absent -> partial; section 6 Wave 1 leftover cleared; formal/ now 15 files,
26 axiom-free closure reports.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

Author: hyperpolymath

.hypatia-ignore

@@ -71,3 +71,5 @@ cicd_rules/vlang_detected:formal/QttTyping.v
 cicd_rules/banned_language_file:formal/QttTyping.v
 cicd_rules/vlang_detected:formal/QttDynamic.v
 cicd_rules/banned_language_file:formal/QttDynamic.v
+cicd_rules/vlang_detected:formal/F5_RenderFaithful.v
+cicd_rules/banned_language_file:formal/F5_RenderFaithful.v

docs/PROOF-NEEDS.adoc

@@ -70,7 +70,7 @@ than the prose corpus suggests:
   `TypeSafety.v` is example lemmas about list length, not AffineScript. Not
   core-metatheory.
 * **`formal/`** — the directory #513 names as the mechanized-proof target now
-  **exists** (Coq/Rocq 8.18), axiom-free throughout — **14 files, 23 `Print
+  **exists** (Coq/Rocq 8.18), axiom-free throughout — **15 files, 26 `Print
   Assumptions` closure reports**, all "Closed under the global context". Codegen
   keystone: `K1_CodegenPreservation.v` (K-1 minimal) +
   `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment).
@@ -79,7 +79,8 @@ than the prose corpus suggests:
   in `P2_Progress.v` (first-order) + `P2_Stlc.v` (STLC with functions + the
   substitution lemma, funext-free) / `P3_BorrowSound.v` (single-bit) +
   `P3_BorrowGraph.v` (multi-resource loan graph) / `F3_PragmaDecidable.v` /
-  `F4_ErrorFaithful.v`. Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) +
+  `F4_ErrorFaithful.v` / `F5_RenderFaithful.v` (render non-collision).
+  Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) +
   `AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative
   typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half:
   β-reduction preserves the usage profile). See <<outstanding>>, <<faces>>.
@@ -302,8 +303,13 @@ cover them.
   renaming of canonical type names, and never collapses two distinct canonical
   types to one face string inside a single message (e.g. Js maps both `Unit` and
   `Option[T]` into "null"-shaped text — show this is unambiguous in context).
-| S | `absent`
-| new; `lib/face.ml` `render_ty`
+| S | `partial`
+| **mechanized** for the vocabulary model: `formal/F5_RenderFaithful.v` proves
+  every face's renaming is injective (`render_inj` — no two canonical types
+  collapse onto one string), incl. the Js/Cafe "null"/"?" overlap
+  (`js_no_collapse`, `cafe_no_collapse`, `option_never_atom`). Faithful to the
+  whole-string Unit/Bool match + canonical-inner Option rewrite; models the
+  name vocabulary, not raw OCaml strings. `lib/face.ml` `render_ty`
 
 | F-6
 | **Preview round-trip totality.** The `preview-{python,js,pseudocode,lucid,cafe}`
@@ -367,8 +373,9 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | **Done.** Grew the models toward the real language: **P-2 → STLC with functions
   + the substitution lemma** (`P2_Stlc.v`, funext-free); **P-3 → a multi-resource
   borrow graph** (`P3_BorrowGraph.v`: loan edges, liveness, move-locality,
-  multi-resource #554 rejected). *Leftover:* F-5 (small, self-contained
-  `render_ty` injectivity) and the K-4 `CAPABILITY-MATRIX` cross-link.
+  multi-resource #554 rejected); **F-5 → `render_ty` non-collision**
+  (`F5_RenderFaithful.v`: every face's renaming injective). *Leftover:* the K-4
+  `CAPABILITY-MATRIX` cross-link.
 | Wave 0
 
 | 2

formal/F5_RenderFaithful.v

@@ -0,0 +1,135 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   F5_RenderFaithful.v
+   ═══════════════════
+   F-5 (docs/PROOF-NEEDS.adoc): `render_ty` faithfulness / non-collision.
+
+   lib/face.ml's `render_ty` rewrites a small fixed vocabulary of canonical type
+   names per face — Unit, Bool, and Option[_] — leaving everything else
+   untouched. F-5 asks: is that renaming injective (it never collapses two
+   distinct canonical types onto one displayed string), even where face lexemes
+   overlap — Js renders Unit as "null" and Option[T] as "T | null", so both
+   mention "null"?
+
+   This models the canonical-type vocabulary render_ty branches on (`cty`), the
+   displayed-name lexemes (`name` — distinct constructors model distinct on-screen
+   tokens), and the rendered form (`rty`), then mirrors render_ty as
+   `render : face → cty → rty`. Two fidelity points carried over from the OCaml:
+
+   * Unit/Bool are special-cased only at the WHOLE-type level (`if s = "Unit"`),
+     never on a nested occurrence.
+   * Option's inner is rendered *canonically* — the OCaml `global_replace`
+     captures the canonical substring `\1` — so Js `Option[Option[Int]]` ⇒
+     "Option[Int] | null" (inner Option intact), exactly the greedy-regex result.
+
+   Theorems: `canon_inj`; `render_inj` (every face's renaming is injective — the
+   non-collapse guarantee); and the pointed `js_no_collapse` / `cafe_no_collapse`
+   / `option_never_atom` (Unit and Option[_] never read as the same type despite
+   the shared "null"/"?" lexeme). Axiom-free, no Admitted.
+
+   Scope (honest): models the displayed-name vocabulary, not raw OCaml strings;
+   assumes well-formed type strings (no adversarial text around `Option[...]`).
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import PeanoNat.
+
+(* The six faces (lib/face.ml `face`). *)
+Inductive face := Canonical | Python | Js | Pseudocode | Lucid | Cafe.
+
+(* Displayed atom lexemes. Distinct constructors ⇒ distinct on-screen names —
+   faithful, because the real renamings (None/null/nothing/bool/boolean/Boolean)
+   are genuinely distinct tokens and no canonical base name equals any of them. *)
+Inductive name :=
+| NUnit | NBool
+| NNone | NNothing | NNull
+| Nbool | NBoolean | NbooleanJs
+| NBase (n : nat).
+
+(* Rendered type forms. *)
+Inductive rty :=
+| RNm (x : name)
+| ROptBr (r : rty)    (* Option[ r ] *)
+| ROrNull (r : rty)   (* r | null    *)
+| RMaybe (r : rty)    (* Maybe r     *)
+| RQ (r : rty).       (* r ?         *)
+
+(* Canonical types: the vocabulary render_ty distinguishes. *)
+Inductive cty :=
+| CUnit | CBool | CBase (n : nat) | COption (a : cty).
+
+(* Canonical rendering — Option's inner stays canonical (matches the regex \1). *)
+Fixpoint canon (t : cty) : rty :=
+  match t with
+  | CUnit     => RNm NUnit
+  | CBool     => RNm NBool
+  | CBase n   => RNm (NBase n)
+  | COption a => ROptBr (canon a)
+  end.
+
+(* Per-face rendering, mirroring lib/face.ml render_ty: top-level special-case
+   for Unit/Bool; per-face Option wrapper with a canonical inner. *)
+Definition render (f : face) (t : cty) : rty :=
+  match t with
+  | CUnit =>
+    match f with
+    | Canonical | Lucid => RNm NUnit
+    | Python            => RNm NNone
+    | Js | Cafe         => RNm NNull
+    | Pseudocode        => RNm NNothing
+    end
+  | CBool =>
+    match f with
+    | Canonical                 => RNm NBool
+    | Python                    => RNm Nbool
+    | Js                        => RNm NbooleanJs
+    | Pseudocode | Lucid | Cafe => RNm NBoolean
+    end
+  | CBase n => RNm (NBase n)
+  | COption a =>
+    match f with
+    | Canonical | Python | Pseudocode => ROptBr (canon a)
+    | Js                              => ROrNull (canon a)
+    | Lucid                           => RMaybe  (canon a)
+    | Cafe                            => RQ      (canon a)
+    end
+  end.
+
+(* ── canonical rendering is injective ──────────────────────────────────── *)
+Lemma canon_inj : forall t1 t2, canon t1 = canon t2 -> t1 = t2.
+Proof.
+  induction t1; destruct t2; simpl; intro H;
+    try discriminate; try reflexivity.
+  - inversion H; reflexivity.                       (* CBase = CBase *)
+  - inversion H; f_equal; apply IHt1; assumption.   (* COption = COption *)
+Qed.
+
+(* ── every face's renaming is injective: the non-collapse guarantee ─────── *)
+Theorem render_inj : forall f t1 t2, render f t1 = render f t2 -> t1 = t2.
+Proof.
+  intros f t1 t2 H; destruct f, t1, t2; cbn in H;
+    solve [ discriminate
+          | reflexivity
+          | inversion H; subst; reflexivity
+          | inversion H; f_equal; apply canon_inj; assumption ].
+Qed.
+
+(* ── the pointed overlaps don't collapse ───────────────────────────────────
+   Js renders Unit as "null" and Option[T] as "T | null"; Cafe as "null"/"T?".
+   The shared lexeme never makes Unit and an Option read as the same type. *)
+Corollary js_no_collapse   : forall a, render Js   CUnit <> render Js   (COption a).
+Proof. intros a H; discriminate. Qed.
+
+Corollary cafe_no_collapse : forall a, render Cafe CUnit <> render Cafe (COption a).
+Proof. intros a H; discriminate. Qed.
+
+(* No Option ever collides with a base/Unit/Bool atom (different rendered shape). *)
+Corollary option_never_atom : forall f a x, render f (COption a) <> RNm x.
+Proof. intros f a x H; destruct f; cbn in H; discriminate. Qed.
+
+Print Assumptions render_inj.
+Print Assumptions js_no_collapse.
+Print Assumptions option_never_atom.

formal/README.adoc

@@ -89,6 +89,11 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **P-4** (Wave 3) — the *dynamic* half: β-reduction preserves the usage profile;
   QTT scaling law; ties back to `usage_soundness`
 | **mechanized**, axiom-free
+
+| `F5_RenderFaithful.v`
+| **F-5** — `render_ty` per-face type renaming is injective (no two canonical
+  types collapse onto one displayed string), incl. the Js/Cafe "null"/"?" overlap
+| **mechanized**, axiom-free
 |===
 
 All mechanized theorems report *Closed under the global context* under `Print
@@ -100,7 +105,7 @@ the obligation shapes as `Definition ... : Prop` over section `Variable`s
 each ending in a `*_discharged : Siblings_Stated.<name> … := <proof>` line that
 type-checks the concrete proof against the stated obligation.
 
-== Mechanized siblings (P-2, P-3, F-3, F-4)
+== Mechanized siblings (P-2, P-3, F-3, F-4, F-5)
 
 Each is proven for a deliberately small concrete model — enough to discharge
 the stated obligation and pin its meaning, not the full language:
@@ -133,6 +138,14 @@ the stated obligation and pin its meaning, not the full language:
 * **F-4** (`F4_ErrorFaithful.v`) — the face renderer preserves an error's
   *class* and *referent*, changing only vocabulary, so no face can make error
   X read as a different error Y.
+* **F-5** (`F5_RenderFaithful.v`) — `render_ty`'s per-face type-name renaming is
+  *injective*: distinct canonical types never collapse onto one displayed string.
+  Models the vocabulary it special-cases (`Unit`, `Bool`, `Option[_]`), faithful
+  to the whole-string Unit/Bool match and the canonical-inner Option rewrite
+  (Js `Option[Option[Int]]` ⇒ "Option[Int] | null"). Proves the pointed case the
+  obligation names — Js/Cafe render Unit as "null"/"?" *and* `Option[T]` with the
+  same lexeme, yet the two never read as one type (`js_no_collapse`,
+  `cafe_no_collapse`, `option_never_atom`).
 
 == Wave 2: the affine/QTT layer (P-4)
 

formal/_CoqProject

@@ -13,3 +13,4 @@ QttSemiring.v
 AffineUsage.v
 QttTyping.v
 QttDynamic.v
+F5_RenderFaithful.v

formal/justfile

@@ -12,7 +12,8 @@ check:
     for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \
              F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \
              P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \
-             QttSemiring AffineUsage QttTyping QttDynamic; do
+             QttSemiring AffineUsage QttTyping QttDynamic \
+             F5_RenderFaithful; do
       echo "== coqc $f.v =="
       o="$(coqc -Q . ASFormal "$f.v")"
       printf '%s\n' "$o"