v4 PROOF-1: external trust-discharge for A3 (no new file)

src/v4/DECISIONS.md

@@ -42,6 +42,7 @@ through — and moves to Part 1.
 | **PAR-1** | Parallelism (T-13) is a THESIS free consequence, a target-AGNOSTIC lens reporting the independence **FACT** (`Witness<ParallelismMap>`); WHETHER/HOW to realize it is target-DEPENDENT — a cost-derived decision (U1/U2 per-target) at emit(T-11)/eval(T-22), NOT the lens. independence = structural-disjointness ∧ effect-independence (consumes `lens/effect.dag`, B3 — Node-disjoint is necessary not sufficient) ∧ fold-combiner associativity-by-inhabitance (consumes `std/algebra.dag` — parallel-reduce is an algebra fact, not a heuristic). fact ≠ spawn-decision; no annotation, no scheduling heuristic. **User-facing contract:** NOT a "parallelize my code" command (forbidden — engine-shaped from the user's seat); a lens the user READS (same UX as complexity/cost); control = structure not a knob; default introspective with the realize-decision derived+inspectable per target (e.g. honestly "no — CPython GIL"); guarantee via `apply_lens(parallelism, Enforce)` (T-23, uniform opt-in-depth). 4 worked examples embedded | `lens/parallelism.dag` header + `TASKS.md` T-13 |
 | **B1** | One content-addressing scheme: a `std`-level Merkle catamorphism `content_hash : Node -> Hash` over the **canonical-form clause** (a SEPARATE explicit node.dag authority — NOT subsumed by A1, which only covers recursion/axis-closure/generics/termination). `Hash` is an opaque digest (no content accessor, K-1-style). One scheme consumed by T-15/T-20/T-21 + A3 + C5. NOT workflow-level | `std/primitive.dag` (`Hash`); `std/node.dag` (canonical-form clause + `content_hash` fold — T-1 worker encodes per relay) |
 | **PARSE-1** | Bodiless `fn` (signature-only / contract-as-checked-signature) is **not needed in the v2-bridge era** (operator-ratified 2026-05-15) — verified by constructive pre-flight: frozen v2's parser **rejects** bodiless `fn` (`expected LBrace`) but cleanly parses the full ratified kernel shape **with bodies** (40k-line `src/v2` corpus + kernel probe, zero syntax errors; the 65 src/v2 errors are 100% post-parse import/cycle). So bridge-era substrate contracts stay **comment-prose** (current scaffold form) and the fail-closed parse-class gate is SAFE — v2 is never asked to parse bodiless fn. **Forward requirement (the conditional that makes the deferral acceptable):** v4's OWN `.dag` grammar (T-7) MUST admit a bodiless signature declaration as a first-class production — graduating the "immutable I/O contract for the worker" from comment-prose to **compiler-enforced** (filled body must conform to the frozen signature; divergence = fail-closed type error, structural per no-annotations). Supportable by construction (v4's own grammar; nothing external constrains it); per B2-OMNI it is a grammar-DATA production, not hardcoded in the walker. v4-self-parser-era only — never through the v2 bridge | `compiler/02_parse.dag` header + T-20 pre-flight note |
+| **PROOF-1** | **External trust-discharge for A3** (operator-ratified 2026-05-15; *not the north star — placed & designed early like AGENT-1*). gunbc's structural evidence (A2 termination descent, the algebra-homomorphism epistemic chain, cost, effects) is EMITTED as a machine-checkable proof term in an external prover (Lean/Coq); their small independently-audited KERNEL checks it. Converts A3's named seed-trust axiom into an INTERSUBJECTIVE check against an anchor gunbc does not own. Does NOT make gunbc un-gameable — the external kernel + the evidence→proof-term faithfulness are the NEW named axioms; it MOVES trust to a stronger anchor (same Trusting-Trust honesty A3 observes). Constraints: the lens EXPORTS witnesses gunbc already has, the prover only KERNEL-CHECKS, never searches (no-engine + A2 "checker not discoverer"); discharges only what is structurally GROUNDED (ungroundable ⇒ fail-closed Diagnostic — inherits gunbc's honesty boundary). Realized as (evidence read) ⊕ (B2-OMNI emit to a `lean`/`coq` language model — ordinary targets); **NO new file** (closed-tree invariant) | `STRUCTURE.md` §7 (A3 home) + `workflow/bootstrap.dag` A3 block + `TASKS.md` T-15 note; cross-ref A2 / AGENT-1 / B2-OMNI |
 
 ---
 

src/v4/STRUCTURE.md

@@ -275,6 +275,32 @@ These are non-negotiable across all v4 work:
    judgment. Not "the substrate refuses.") This surfacing structure is in
    force from scaffold time; the tasks fill behavior *under* it.
 
+   **PROOF-1 (operator-ratified 2026-05-15) — the external trust-
+   discharge for A3.** A3 is honest that the guarantee is *un-hideable*,
+   not *impossible-to-violate*, and that seed trust is a named axiom.
+   PROOF-1 is the mechanism that SHRINKS that trust surface: gunbc's
+   structural evidence — A2 termination descent, the algebra-homomorphism
+   epistemic chain, the cost bound, the effect facts — is EMITTED as a
+   machine-checkable proof term in an external proof assistant
+   (Lean/Coq); their small, independently-audited KERNEL checks it. This
+   converts "trust gunbc's internal checker + the frozen seed" into an
+   INTERSUBJECTIVE check against a trust anchor gunbc does not own. It
+   does NOT make gunbc un-gameable — the external kernel + the
+   faithfulness of the evidence→proof-term emission are the NEW named
+   axioms; PROOF-1 *moves* trust to a stronger anchor, it does not
+   eliminate it (the same `feedback_no_engine`/Trusting-Trust honesty A3
+   itself observes). Hard constraints: (i) the lens EXPORTS witnesses
+   gunbc ALREADY HAS (the descent evidence, the homomorphism) — the
+   external prover only KERNEL-CHECKS, it never SEARCHES for a proof (a
+   searching export would violate no-engine + A2 "checker not
+   discoverer"); (ii) it discharges only what is structurally GROUNDED —
+   ungroundable concepts remain fail-closed Diagnostics; PROOF-1 inherits
+   gunbc's honesty boundary, it does not paper over it. Realized as a
+   lens = (evidence read) ⊕ (B2-OMNI emit to a `lean`/`coq` language
+   model — ordinary emit targets, no new subsystem); NO new file (the
+   closed-tree invariant holds). Primary export source = A2; an agent may
+   REQUEST it (AGENT-1).
+
 8. **On-disk emitted artifacts are checked projections, not authority
    (C4, operator-ratified 2026-05-15).** Some emitted artifacts must live
    on disk because an external tool reads them from the repo (GitHub

src/v4/TASKS.md

@@ -75,6 +75,14 @@ Phase 3 (parallel — lens dimensions):
 Phase 4 (serial — close the loop):
   T-14  test/claim/* + test/fixture/* (port load-bearing TestClaims from v3)
   T-15  bin/main.dag + bootstrap glue + self-host fixed-point validation
+        + PROOF-1: the external trust-discharge for A3 — a lens =
+          (evidence read: A2 descent, algebra-homomorphism chain, cost,
+          effects) ⊕ (B2-OMNI emit to a lean/coq language model). The
+          prover KERNEL-CHECKS gunbc's exported witnesses (never
+          searches — no-engine + A2). No new file; framing in
+          STRUCTURE.md §7 + DECISIONS.md PROOF-1. Realized when the
+          lens framework + a lean/coq model land (composition, not a
+          new subsystem).
   T-16  Full-stack omni-emission demo: ONE .dag → Rust+C++ backend
         + React/TS frontend + OpenAPI wire contract
         [needs T-4, T-4.5, T-4.6, T-4.7, T-4.8, T-10, T-11]

src/v4/workflow/bootstrap.dag

@@ -48,6 +48,17 @@
 //   - A4 corollary: a 7th connective / 6th behavior is the SAME machine —
 //     it changes the reproduction → conspicuous signal → STOP → human
 //     judgment. Not "the substrate refuses by construction."
+//   - PROOF-1 (operator-ratified 2026-05-15) — the EXTERNAL trust-
+//     discharge: gunbc's structural evidence (A2 descent, the algebra-
+//     homomorphism chain, cost, effects) is emitted as a machine-
+//     checkable proof term an external Lean/Coq KERNEL checks. Converts
+//     the seed-trust NAMED AXIOM above into an INTERSUBJECTIVE check
+//     against an anchor gunbc does not own — does NOT make it
+//     un-gameable (the external kernel + evidence-faithfulness are the
+//     new named axioms; trust MOVED, not eliminated). The lens exports
+//     witnesses already held; the prover only kernel-checks, never
+//     searches (no-engine + A2). Full framing: STRUCTURE.md §7 +
+//     DECISIONS.md PROOF-1.
 //
 // Discipline:
 //   - This file is the ONLY bootstrap authority. No build.rs, no bootstrap.sh.