From 576d205cf7d8011a2110c2d82d491d005c6a52cf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 15 May 2026 16:40:43 -0400 Subject: [PATCH] v4 PROOF-1: external trust-discharge for A3 (no new file) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operator-ratified 2026-05-15 (option b, AGENT-1-style placement — no new file). 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. This is the honest completion of A3: it converts A3's named seed-trust axiom into an INTERSUBJECTIVE check against an anchor gunbc does not own. It does NOT make gunbc un-gameable — the external kernel + the evidence→ proof-term faithfulness are the NEW named axioms; trust is MOVED to a stronger anchor, not eliminated (same Trusting-Trust honesty A3 states). Constraints: the lens EXPORTS witnesses gunbc already has, the prover only KERNEL-CHECKS (never searches — no-engine + A2 checker-not- discoverer); discharges only structurally GROUNDED claims (ungroundable ⇒ fail-closed Diagnostic). Placed in A3's homes: STRUCTURE.md §7 + workflow/bootstrap.dag A3 block + DECISIONS.md PROOF-1 row + TASKS.md T-15 note. Realized later as a composition (evidence read ⊕ B2-OMNI emit to a lean/coq model) — no new file, closed-tree invariant preserved. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/v4/DECISIONS.md | 1 + src/v4/STRUCTURE.md | 26 ++++++++++++++++++++++++++ src/v4/TASKS.md | 8 ++++++++ src/v4/workflow/bootstrap.dag | 11 +++++++++++ 4 files changed, 46 insertions(+) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 2904436e269..dd174059478 100644 --- a/src/v4/DECISIONS.md +++ b/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`); 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 | --- diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index 056536a24d5..7feb81dc456 100644 --- a/src/v4/STRUCTURE.md +++ b/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 diff --git a/src/v4/TASKS.md b/src/v4/TASKS.md index 5ed7f51ffdb..3b1a7e48862 100644 --- a/src/v4/TASKS.md +++ b/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] diff --git a/src/v4/workflow/bootstrap.dag b/src/v4/workflow/bootstrap.dag index 94ffacbb236..f32f7a3a3b7 100644 --- a/src/v4/workflow/bootstrap.dag +++ b/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.