Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
357 lines (281 loc) · 17.5 KB

AFFIRMATION.adoc

File metadata and controls

357 lines (281 loc) · 17.5 KB
Raw

AFFIRMATION — tangle, as of 2026-06-19

the No-Bullshit file: what we affirm was true and checkable at this moment

Note

Genre. An affirmation is a solemn declaration of the truth of a statement, made by someone who declines to swear an oath — our truth-as-best-believed at a stamped instant, binding on our honesty, not a claim of infallibility. It is not the README and not the EXPLAINME:

File Answers Tense

README.adoc

Where is this going, and why? — Tangle’s purpose and steering

future / aspirational

EXPLAINME.adoc

How is it built, and what’s the evidence?

descriptive / mechanism

AFFIRMATION.adoc (this file)

What can we honestly affirm was true and checkable at a stamped moment?

a frozen instant, falsifiable

Every repo in the estate carries one, per the 2026-06-19 estate rule.
Table of Contents

What this is, and how it is designed to work

What it is. A short, dated, jointly-signed snapshot of what we can honestly and verifiably claim about the tangle repo at one exact commit.

How it is designed to work.

  1. Ground truth, not memory. Every gate result below was produced by running the check this session. Material caveat (read it): just is absent, so RSR/ contractile checks were run as bash; and none of tangle’s build/test/proof toolchains were runnable this session — cargo build --offline could not resolve dependencies (no vendored crates / no network), and OCaml dune + Lean are not installed. See [Outstanding / not-run].

  2. A frozen anchor. The file names the exact commit SHA, branch, and toolchain (see Verifiable anchor).

  3. A real signature. Authoritatively landed by the maintainer’s signed git commit. The AI engineering party cannot GPG-sign and does not claim to.

We are fallible. Best honest belief, not a proof of its own correctness.

The epistemic contract

This document records our best joint belief at the timestamp below. No intentional overclaim: where a check passed we say "PASS"; where the toolchain was absent we say "not run", never "passed".

Standing invitation to refute. Reproduce Reproduce it yourself at the stamped commit and tell us where the discrepancy is.

Verifiable anchor

Repo

hyperpolymath/tangle — Tangle / KRL topological programming language: the proven type-safe small-step core + canonical TangleIR

Branch

claude/practical-newton-9eFe2 (feature branch; not anchored to main)

Commit (HEAD)

102499dbacb005bb5adc46736c8798fa1d365a82

Permalink

https://github.com/hyperpolymath/tangle/tree/102499dbacb005bb5adc46736c8798fa1d365a82

Verified

2026-06-19 (checks run this session; precise UTC second not captured — date, not claimed instant)

Working-tree delta

Clean — git status --porcelain shows only this untracked AFFIRMATION.adoc. (The README stack-diagram edit placing VerisimCore is maintainer-confirmed and is committed in the parent commit 102499d.)

Toolchain (present)

git, Agda 2.6.3, rustc, cargo. Absent this session: just, deno, julia, lean, OCaml dune.

Run method

RSR/contractile gate bodies as bash. cargo build --offline attempted (dep-resolution failure — not a code verdict). OCaml + Lean not run (absent).

HEAD commit signature

Not signed by the AI party. Authoritative signature is the maintainer’s signed commit that lands this file.

Stack placement: VerisimCore (maintainer-confirmed 2026-06-19)

The architecture ladder in README.adoc was updated and confirmed correct by the maintainer on 2026-06-19. The canonical stack now reads:

KRL (surface language)
  ↓
TangleIR (canonical representation)
  ↓
VerisimCore (categorical abstraction)
  ↓
Skein / QuandleDB (storage and equivalence)

This resolves the previously-parked VerisimCore-placement question — VerisimCore sits between TangleIR and the storage/equivalence layer as the categorical abstraction. The edit is committed in the parent commit 102499d (not uncommitted). It simplifies the diagram’s labels; the finer estate framings (e.g. "KRL is not merely a query language", "Skein is the engine") continue to live in krl’s and Skein.jl’s own docs and affirmations.

Companion documents and repo metadata (cross-check)

  • README.adoc — title = Tangle / KRL — Topological Programming Language (real). Now carries the maintainer-confirmed VerisimCore stack (committed, parent 102499d).

  • EXPLAINME.adoc — present, real: = EXPLAINME: Tangle.

  • 0-AI-MANIFEST.a2ml — present.

  • Template residue — 5 files still contain {{PLACEHOLDER}} tokens and 8 files reference the rsr-template-repo lineage. The Justfile itself is clean of the template name. Partial instantiation debt — noted, not hidden.

  • GitHub repo description / topics — not fetched this session (no gh).

The honest state (one breath)

tangle is the most rigorous repo in the estate so far: a serious multi-language implementation — an OCaml compiler core (compiler/{bin,lib,test}
dune-project), Rust crates (src/rust with a committed Cargo.lock, compiler/tangle-lsp, compiler/tangle-wasm), Lean-4 type-safety proofs (proofs/Tangle.lean, proofs/TG3Differential.lean, lean-toolchain), grammars, and five dialects. It self-grades READINESS C and documents real formal verification, and its stack placement (incl. VerisimCore) is maintainer-confirmed. The honest gaps: some template residue remains, and — crucially — none of its build/test/proof toolchains were runnable this session, so what follows confirms structure and the repo’s own proof ledger, not a fresh green build.

What is solid (and how we checked)

  • MUST/TRUST-style checks — PASS. Run as bash: LICENSE present; no banned Dockerfile/Makefile; SPDX headers on a sampled 120 .rs files (0 unheadered); LICENSE carries an SPDX/MPL identifier; no .env / credentials.json committed.

  • Real, substantial, multi-language content. OCaml compiler (compiler/lib, compiler/bin, compiler/test, dune-project); 18 Rust source files with a pinned Cargo.lock; LSP + WASM Rust crates; grammars (src/tangle.ebnf, src/tangle-jtv.ebnf, spec/grammar.ebnf); Lean proofs; five dialects (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot).

  • Documented formal verification (the repo’s ledger, reported as such). PROOF-NEEDS.md records TG-3 LANDED at translation-validation level: 496 Lean kernel-checked obligations in TG3Differential.lean (generated from infer_expr, by decide) + 1008 OCaml --check assertions (dune runtest), reduced via TG-2 (infer ≡ HasType). We report this as tangle’s own documented status — we did not re-run Lean/OCaml this session.

Known-incomplete but honestly fenced (loud, never silent)

  • READINESS grade C. READINESS.md self-assesses Current Grade: C — reported as-is.

  • Template residue. 5 {{PLACEHOLDER}} files + 8 rsr-template-repo references remain to be cleaned.

  • Proof scope is honest in the repo’s own words: TG-3 refinement is OCaml→Lean only (not a universal Lean proof over all OCaml runs); bool==bool and the close boundary are catalogued divergences (D1/D2). We do not inflate it.

Outstanding / not-run (no spin) [[Outstanding / not-run]]

  • No build/test/proof toolchain was runnable this session.

    • cargo build --offline failed to resolve dependencies (serde, … are not vendored and offline mode cannot fetch them). This is an environment limit, not a code verdict — Cargo.lock is present; a networked cargo build/cargo test in-environment is the authoritative check.

    • OCaml dune and lean are absent, so the compiler test suite and the Lean proofs were not executed. We affirm the proof files exist and report the repo’s documented TG-2/TG-3 status — we do not affirm, from this session, a fresh green proof/build.

Reproduce it yourself

From the repo root, at the commit above:

git rev-parse HEAD          # expect 102499dbacb005bb5adc46736c8798fa1d365a82
git status --porcelain      # expect only this untracked AFFIRMATION.adoc

# MUST / TRUST style (expect PASS):
test -f LICENSE; test ! -f Dockerfile -a ! -f Makefile
grep -q 'SPDX\|MPL' LICENSE; test ! -f .env

# Instantiation debt (expect residue):
grep -rl '{{'{{'}}[A-Z_]*{{'}}'}}' --include='*.adoc' --include='*.md' . | grep -v PLACEHOLDERS  # ~5 files
grep -rl 'rsr-template-repo' . | grep -v '.git/'                                     # ~8 files

# The honest gaps (NOT runnable without env/toolchain):
#   ( cd src/rust && cargo build )        # needs network or vendored deps
#   ( cd compiler && dune runtest )       # needs OCaml/dune
#   bash proofs/check-tg3-differential.sh # needs Lean

One-line characterisation (quote this)

"Tangle is the proven type-safe small-step core + TangleIR of the KRL stack (KRL → TangleIR → VerisimCore → Skein/QuandleDB, maintainer-confirmed) — a serious multi-language implementation (OCaml compiler, Rust LSP/WASM with a pinned Cargo.lock, Lean-4 type-safety proofs, five dialects) that self-grades READINESS C and documents real formal verification (TG-3 translation-validation LANDED: 496 Lean obligations + 1008 OCaml assertions, per its own proof ledger). MUST/TRUST gates pass; honest debt: 5 placeholder files + 8 rsr-template-repo references remain, and none of its build/test/proof toolchains were runnable this session (cargo offline can’t resolve deps; OCaml/dune + Lean absent) — so structure + the repo’s proof records are confirmed, not a fresh green build. No intentional overclaim."

Key concern + cross-repo wiring

tangle’s key concern is type-safe semantics + the canonical TangleIR — the proven small-step core that KRL lowers into and that the categorical / storage / equivalence layers build on. Per the 2026-06-19 estate rule, each repo carries its own AFFIRMATION + scoped Must/Intend/Wish table; tangle’s lives at docs/identity-fabric/musts-intends-wishes.adoc. Confirmed stack: krl (surface DSL) → tangle (TangleIR + type-safe core, this repo) → VerisimCore (categorical abstraction) → Skein.jl / quandledb (storage + equivalence). Adjacent: echo-types — structured-loss theory + the identity-fabric framing.

Joint attestation

To the best of our joint belief at the timestamp above, every claim in this file is true and was checked as described — with no intentional overclaim and with the un-run toolchains stated rather than implied.

  • Engineering party (AI): ran the RSR/contractile checks recorded here as bash on 2026-06-19, attempted the offline cargo build, committed the maintainer-confirmed VerisimCore README edit, and stands behind this wording as a faithful report — including the toolchain-absent caveats and explicitly not having re-run the Lean/OCaml proofs.

  • Owner / maintainer: Jonathan D.A. Jewell — signs by committing this file with -S; the signed git commit over this content, at the SHA above, is the authoritative form.

  • Signed-off-date: (fill on signing)

Erratum — 2026-07-21

This section corrects the affirmation above. The original text is left intact: an affirmation is a dated claim about a past state, and amending it in place would falsify a record. Two of its claims have since been shown to be wrong, and one of its acknowledged gaps has since been closed.

Correction 1 — the stack does not exist

The affirmation records, as maintainer-confirmed, the ladder:

KRL -> TangleIR -> VerisimCore -> Skein/QuandleDB

TangleIR does not exist. The identifier appears in no source file in this repository (0 hits across .rs, .zig and .lean) and in no source file in the KRL implementation at quandledb/server/krl/. It existed only in prose, in both repositories, and has been removed from README.adoc.

Nor is KRL a surface language for Tangle. KRL is QuandleDB’s resolution language, developed jointly with QuandleDB; it neither compiles to nor depends on Tangle. The three projects share a subject matter, not an architecture.

The confirmation recorded on 2026-06-19 was a confirmation of the README’s diagram, and that diagram was wrong. Nothing here suggests bad faith — the affirmation is careful, and states plainly which of its checks were not run.

Correction 2 — the "one-line characterisation" should not be quoted as-is

The characterisation invites quotation. It should not be quoted while it describes Tangle as "the proven type-safe small-step core + TangleIR of the KRL stack". Everything else in that sentence survives: the OCaml compiler, the Rust LSP/WASM targets, the Lean 4 proofs and the five dialects are all real.

Discharge — the Lean proofs have now been run

The affirmation states: "OCaml + Lean not run (absent)", and concludes that "structure + the repo’s proof records are confirmed, not a fresh green build".

That gap is now closed for Lean. On 2026-07-21 the repository’s own documented oracle was executed:

$ cd proofs && lean Tangle.lean
$ echo $?
0

Exit 0, no errors, using the pinned toolchain from proofs/lean-toolchain (leanprover/lean4:v4.14.0). The proofs are self-contained — Tangle.lean has no import lines at all, so no Mathlib — and contain zero occurrences of sorry and zero axiom declarations across 2,128 lines. progress, preservation, determinism, type_safety, infer_sound, infer_complete and infer_iff_hasType are all present with real proof terms.

This matters because "the Lean build is green" and "the theorems are proved" are not the same claim in general: an axiom stub compiles cleanly while proving nothing. Here they coincide, and that was checked rather than assumed.

The OCaml compiler remains unbuilt — no workflow in this repository builds it.

Erratum — 2026-07-29

A second dated correction, appended under the same convention: the text above is left intact, because an affirmation is a claim about a past state and amending it in place would falsify a record.

Correction 3 — the template residue is cleared

The affirmation records as honest debt:

5 {{PLACEHOLDER}} files + 8 rsr-template-repo references

Both counts were low, and the classification conflated two different things. Re-measured 2026-07-29: 8 files matched {{…​}} and 21 lines matched rsr-template-repo — but most were meta-references, i.e. files describing the debt rather than carrying it. Three are worth naming, because a naive search-and-replace would have damaged them:

  • src/rust/src/eval.rs — "…​add{{}} block" is a Rust format! escape ({{}} renders as a literal {}) describing the add{} language construct. It is code, not a placeholder.

  • .machine_readable/bot_directives/methodology.a2ml — the string appears inside reject-if-contains, which exists precisely to forbid it.

  • AFFIRMATION.adoc (this file) and docs/identity-fabric/ — prose recording the debt.

The genuine residue was: {{DEPS}}, {{BUILD_OUTPUT_PATH}}, {{PACKAGE_NAME}} in QUICKSTART-MAINTAINER.adoc; {{LANG_STACK}}, {{BUILD_CMD}}, {{TEST_CMD}}, {{MUST_INVARIANTS}} in QUICKSTART-DEV.adoc; {{PROJECT_UNIQUE_STRENGTH}} in methodology.a2ml; and four contractiles (Intentfile, Trustfile, Mustfile, Adjustfile) plus docs/CITATIONS.adoc whose subject was still rsr-template-repo — Intentfile asserted "This repository is the canonical template for Rhodium Standard Repository compliance", and the citation guide credited "Polymath, Hyper" for "RSR-template-repo". All are now instantiated for tangle.

A worse class surfaced while fixing it: both QUICKSTARTs documented commands that do not exist — just build, just test, just lint, just panic-scan, just setup-dev, just build-release, just install, just run, just stapeln-export — and asserted an $XDG_CONFIG_HOME/tangle/config.toml that the compiler never reads. Documentation that fails when followed is worse than none, so the recipe lists are now checked against just --list by scripts/check-rsr-instantiation.sh.

Correction 4 — the OCaml compiler is no longer unbuilt

The closing line of the 2026-07-21 erratum reads:

The OCaml compiler remains unbuilt — no workflow in this repository builds it.

That was true when written and is no longer. .github/workflows/ocaml-ci.yml (added 2026-07-29, PR #87) builds the compiler and runs the full suite — over 4,000 assertions — on every relevant push and PR, and PR #89 added a gate over the runnable corpus (examples/ + conformance/).

That gate immediately earned itself: examples/isotopy.tangle, the program whose purpose is to demonstrate the language’s central claim, was failing its own assertions and had been for as long as ~ used free reduction. It passes only since TG-7 (#50/#87) made ~ decide real braid-group equivalence.

Correction 5 — == is no longer list equality

Anywhere the affirmation or its sources describe braid == as list equality: that ceased to be true on 2026-07-29. Owner ruling #50 chose braid-group equivalence, implemented in PR #87 across both engines. The metatheory is proven relative to the decision procedure; its correctness is registered as assumption A-TG-7.2 and is not claimed as proven.