Repository navigation
feat(wordram): prepare ExactTriangle instances from initialized input - #1611
Merged
SamuelSchlesinger merged 72 commits intoOct 29, 2026
Merged
Conversation
Adapt the finite counting interface and signed digit expansion from anthropics/formal-math@16a5ce4 for milestone #1438. This is a mathematical interface; native preprocessing, fast solvers and full composition remain under #1394.
Adapt the complete finite Theorem 17 splitting and recovery component, using the existing three weight matrices, lopsided graphs, modular counts and EqOn answer interface. Prove exact integer/real capacity bridges so the finite constructions and scans are computable. Preserve Anthropic source credit; keep the native 3SUM endpoint open in #1394. Validation: all six gates in scripts/check.sh pass, with LEAN_NUM_THREADS=1 and cache downloads disabled after bootstrap. Full hygiene, changed-source check-simp, changed-file lints and git diff --check pass. Curated abstracts and rendering are unaffected. AI-assisted implementation/self-review by Codex worker codex-three-sum-splitting-t3-0a4d90c0; independent review will be recorded in the PR.
Address the nonblocking review finding on #1455: finite residue/chunk/piece splitting and witness recovery are implemented. Preserve native preprocessing, fast solvers, full input/time/width composition and exponent 1.9992 as open work under #1394. Documentation only. Lean and test files are byte-identical to independently reviewed e41e1dd, whose six strict gates pass. Checked the diff, milestone reference, implementation paths, hygiene and changed-file lints. Abstracts and rendering are unaffected.
Implement fixed native residue, histogram and composed collision-counting programs with explicit frames, local word-fit contracts, exact mathematical collision semantics and charged bound 34n + 5M + 18 (halt excluded). Implementation layer for #1454 under #1446/#1394, not full preprocessing. Sorting/frontend, prime searches, heavy extraction, recursion/output and global logarithmic-width/subquadratic-time composition remain open. Curated abstracts: no impact on headline statements, definitions or scope. Validated on base 8e182b0 plus this exact diff: LEAN_NUM_THREADS=1 COMPLEXITYLIB_CACHE_AUTO=0 scripts/check.sh: all six gates passed, including strict test/global axiom audit. Changed-file lints against that base, hygiene --check-simp and git diff --check passed. Final run followed resolution of shared-host disk/memory pressure; failed earlier attempts are not counted as validation. Independent read-only agent correctness/API review by /root/review_native_histogram approved the final source blobs after replacing three private clear helpers with WordRAM.clear. No remaining blockers; optional Count parameter-frame API can accompany its minimum-search client. This is within-fleet agent review, not outside-coordinator or human approval. Outside coordinator review is required before integration. AI assistance: OpenAI Codex implementation/self-review and a separate Codex review context. Native programs/counting proofs are original; existing Anthropic mathematical source credit is preserved unchanged.
Implement the complete finite mathematical milestone of #1463 above #1464: valid layouts, batch-product correctness/error exclusion, arbitrary-N tiling, exact requested signed products, order/cardinality estimates, geometric tails and the derived sparse bounds. At D=4^m, L=19m, D^18<=N and |W|*2^m<=N^2, encoding entries are bounded by4*N^2/D^(1/18), contributing leaves by33 and passed-set cardinalities by(19m+1)*33 times that scale. Add finite magnitude and auxiliary object-count bounds. None are native instruction costs. All six final local gates pass: strict build, aggregate check, strict tests, environment lint, style lint and init-import check. Hygiene --check-simp, changed-file lints (14 library modules,1 new test) and diff --check pass. Tests kernel-check signed results3,20,0,-8, true padding, empty/sparse and negative-order boundaries, and instantiate all aggregate bounds with jointly satisfiable m=1 parameters and symbolic matrices without resource overrides. Read-only math/API review by /root/thin_product_review is clear after fixed doc references/magnitude wording/quotation hygiene. Focused final delta review by /root/thin_product_final_delta_review is clear for tree b021e2d, reusing the prior mathematics review. These are internal agent reviews, not outside coordinator or human approval. Source: anthropics/formal-math@16a5ce4, selective Section2 finite mathematics; Anthropic credit/NOTICE retained. Abstract assessment: no impact on selected headlines, catalogue or rendering. Full native tensor/sparse-product/Exact Triangle code, native Chan-He #1446, whole input/time/width composition and improved1.9992 remain under #1394. AI assistance: implementation and reviews with OpenAI Codex, worker session codex-thin-product-math-20261028.
Implement fixed 24-register parameter code with charged numeric helpers, exact existing Chan–He outputs, preserved input memory, derived logarithmic width and subquadratic native time. Add executed boundary and input-init contract examples. Original implementation and proofs credited to Erik Demaine; AI assistance by OpenAI Codex. Part of #1446; independent complete parameter subtask #1458.
Restack #1463 above repaired #1464 without changing the reviewed mathematics. Rewrite 149 documentation blocks in 14 modules as standalone descriptions; replace operation-cost and word-size narratives with the exact entry, leaf, passed-set and specified-value quantities proved. Preserve pinned Anthropic credit, source locators, statements, definitions, proof bodies and imports. An independent comparison with original ee288fb confirms that all code bytes outside comments are identical, including code whitespace. Validation of this final tree: all six gates pass together (strict build, aggregate check, strict tests, environment lint, style lint, init imports). Citation-aware full hygiene --check-simp, changed-file lints (14 library modules, one test) and git diff --check pass. Lean MCP FiniteMagnitude diagnostics finish without errors or warnings. Serial Smoke/Axioms warmups avoid the shared-host memory failure previously seen when these import-heavy clients run together. Tests and substantive math/API review evidence are retained from the original reviewed tree b021e2d in ee288fb. This change is documentation-only; /root/draft_thin_docs authored the scratch map and the continuation worker inspected/applied it. That drafting is not independent review. Earlier math reviews are inside-fleet agent reviews, not outside or human approval. Outside coordinator review will be requested on the final PR. No selected abstract, catalogue or rendering is affected. PR publication remains held while native dependent restacks are repaired, per root sequencing. #1394 remains open: native shared encodings/pruning/Exact Triangle, Chan-He #1446, complete Convolution/ordinary input/time/width composition and the improved Section4 route to exponent1.9992 are not supplied by these finite counts. AI assistance: OpenAI Codex workers codex-thin-product-math-20261028, codex-three-sum-continuation-t3-3dda8289 and /root/draft_thin_docs.
Complete the shared left/right encoder milestone #1493 above parent b4936ce (#1496). Fixed standard-WordRAM code with 32 registers computes every public encodingL/encodingR leaf from actual initialized flat signed inputs. The native bound is 240*(L+1)*10^L instructions plus halt, with explicit magnitude/address inequalities, two alternating buffers, charged initialization/copying and the complete outside frame. The full ordinary native 3SUM objective #1394 remains open; this component supplies no sparse-query or Exact Triangle solver. Validation of tree b598513 against b4936ce: all six gates pass together (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), full citation-aware hygiene --check-simp, changed-file lints (13 library modules, one new test) and diff checks pass. Tests execute both encoders at depths zero, one and two, compare all 100 depth-two leaves with the unchanged public encodings, preserve input/frame sentinels, and cover adjacent word widths and all three copy block orders. Kernel-checked concrete flat executions discharge every width/magnitude premise. Selected abstracts, catalogue and rendering are unaffected. AI assistance: OpenAI Codex implementation and self-review by delegated worker codex-shared-encoding-t3-03b600bd. Independent correctness/API review is pending; this is not an approval or a claim that the complete 3SUM objective is done.
Connect the zero-depth and two-stage regression memory witnesses to the actual prefix Runs already proved by runs_left, rather than discarding that conjunct. Bound the prefixes by 240 and 72000 instructions and expose the same executions' charged halt at n+1. All library code is unchanged from ad3e097 (tree b598513). Validation of tree 8277017 against actual parent b4936ce: all six gates pass together (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), full citation-aware hygiene --check-simp, fresh changed-file lints (13 library modules, one test), strict PR-draft declaration-name check and staged/unstaged diff checks pass. Independent nonauthor agent review 8034f3da approved exact ad3e097/tree b598513, covering full code/model/cost/width/source and ArrayCopy with no blockers. It is inside-fleet review, not outside approval. This test-only delta addresses its optional witness-connection finding; focused final test/source-mapping review remains pending through the parent coordinator. No selected abstract, catalogue or rendering impact. The full ordinary native 3SUM objective #1394 remains open; this implements encoder issue #1493. AI assistance: OpenAI Codex implementation/self-review by delegated worker codex-shared-encoding-t3-03b600bd. Publication remains on hold for focused review; this commit is not approval or a whole-3SUM completion claim.
…ee-sum-native-et-instances-20261028
…ee-sum-native-et-instances-20261028
Address the bounded nonblocking review findings on #1496. Keep Nat.choose_le_exp_mul_div_pow unchanged while deriving it from Cslib.sum_choose_le_exp_one_mul_div_pow in the existing real binomial module; remove the redundant module and migrate its import. Preserve Anthropic, Samuel Schlesinger, OpenAI and Erik Demaine credit. Kernel-check an actual mixed inner/outer L2,m1 signed pruned result of -8, remove two signature-only tests and retain positive admitted-parameter checks. Paraphrase the identified source-derived sentence, shorten generic source boilerplate and record the generic naming follow-up. No public mathematical statement or definition changes meaning; no selected abstract or endpoint promotion. Final validation/source/review evidence is in PR #1496. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
Partial work for #1532 under the still-open #1394 endpoint. Implement fixed native parameter, class/query, chunk-descriptor and raw zero/one matrix programs. Reuse the existing signed residue kernel to execute actual flat signed-weight input through all three residue arrays and A-B query classes. Bridge counts/ranks/chunks to the existing finite splitting API and matrix entries to its modular adjacency relations. Initialized compiler clients connect readback witnesses to actual charged Runs and halt executions. This checkpoint does not complete #1532: whole catalogue/instance composition, derived logarithmic-width bounds and the aggregate preparation estimate remain open. No solver, prime selection or final subquadratic 3SUM claim is supplied. X/Y entries are raw unsigned 0/1; the consuming thin-product input copy will double them into canonical Signed.encode words with charged instructions. Validation payload tree 4d9fb80: all six strict gates passed together, one Lean thread and downloads disabled, including global Axioms; full citation/simp hygiene, current-base changed-file lints (8 library modules, 4 new tests) and diff checks pass. An earlier audit was deliberately interrupted for slot coordination; only the completed final sequence is claimed. Curated abstracts: no impact, no new headline selected. Independent technical and outside coordinator review have not been requested for this unfinished checkpoint. No PR is opened by this commit. AI assistance: OpenAI Codex implemented and checked this checkpoint. Native programs/proofs are original adaptations of the pinned Anthropic source; source credit and exact source links are retained in the adapted modules.
Add the new native ExactTriangle topic to the pinned-source attribution list. Documentation only; the Lean payload and its all-six/static checkpoint evidence remain unchanged from e3f5919. No curated abstract impact. AI assistance: OpenAI Codex.
Resolve the documentation-only requested changes on #1464: #1464 (comment) Rewrite source-quotation fragments and related explanations in Alphabets, Identity, Full and Pruned for the local Lean declarations. Preserve the mathematical attribution, bibliography keys, source pin and copyright. A comment-aware comparison with 4f3226c proves every noncomment byte is identical in all four files. No declaration, proof, definition, program, import or test changes. Existing checked source-statement quotations and notation/quantifier/model/resource mapping in the PR remain unchanged. The final source-comment screen compares against quoted fragments in the actual pinned Sec2 and Statements/PaperStatements files, including the known local renames; no substantial quoted fragment remains unmarked. Validation is recorded for this exact tree in PR #1464. Source checkpoint tree 8c3b87b. No abstract/catalogue/model/scope or rendering impact; no new headline. The full native 1.9992 endpoint remains open under #1394. Ancestor and descendant remotes are unchanged. AI assistance: documentation repair and validation by Codex continuation worker codex-three-sum-continuation-t3-3dda8289. Existing independent mathematical/API and checked-source review coverage is retained; outside review of the bounded documentation delta is requested, with no new review agent commissioned.
…ee-sum-native-et-instances-20261028
…tor/refresh-1520-landed38-20261029
Complete the native preparation milestone #1532 above the original kernel checkpoint. Fixed64 native code computes parameters, signed residues, actual classes/query arrays/chunks and every record with raw n-by-D/D-by-n adjacency matrices from the original input. Same-y State.init Runs plus charged halt, exact finite readback/unique indices, full frames and derived fits are proved. Source-regime cost is690n^2 Dg including halt. With size-bounded scalar headers and A<=(n+2)^kappa, physical width is at most(kappa+18)clog2(n+2); every prefix's words and address support lie below(n+2)^(kappa+19). No run/layout/time/solver oracle. Prime selection, product/backend1581 and the full1394/1.9992 remain open. Validation tree5a46782a1f51dee866e5c08f0c884f2bdf14a240 on reviewed encoder parent6dbd0cc45f8cfba188c1a8211b8b8f15d78c59f6: all SIX strict gates passed together, LEAN_NUM_THREADS=1 and cache downloads disabled during the sequence, including Smoke/global Axioms; full citation/simp/heartbeat hygiene, actual-base 22-library/6-new-test lints,18 strict PR-body names and diff checks passed. Source cases include signed tiny input, nonzero scratch/sentinels, shortchunks, padding, insufficient-width faults, and a fully admitted n=D16,g1,p3 client. The earlier interrupted cold-build checkpoint is not claimed as validation. Nonauthoring native reviewer /root/et_preparation_review read the full own layer at treea72db19345fa47bec57a62cea61d9c1b22b8a2c4, then approved the focused final delta at5a46782a with no blockers/P2 findings. The ten executable-mode nits were fixed; other final deltas are comments and exact already-reviewed supplier parameter-budget metadata from1469@4b2d75ce, reduction tracked1583. All program/public-statement/proof meanings unchanged by those deltas. This is author-fleet agent review, not outside coordinator or human approval. Quote and source mapping checked directly at Anthropic formal-math pin 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, Sec3/Theorem17/Instances/ WriteMatrices.lean:15. Finite classes/chunks/lopInstance are reused. New native instruction coefficients are original; source Light costs/full host not claimed. Generic Width/Fits files are exact reviewed1537/1552 copies; other reviewed native prerequisites retain their source credit. Selected abstracts/rendering are unchanged; no new headline is promoted. AI assistance: OpenAI Codex implemented, checked and documented this native composition; separate nonauthoring agent reviewed correctness/API/source scope.
…tion Adopt actual reviewed1520 parentd2e8386e (outside FINAL6489625410), including landed finite API cleanup1556 and native arithmetic1469. Preserve both encoder and preparation ROADMAP milestones. Migrate preparation-bound hypotheses and the admitted sourcecase only to Nat.sqrtPrimeWindow and its square test. Every native program and all other preparation source/test bytes are unchanged. Final validation treef728d30c4c70e0f5e70e4ddfef744a5d2e3817b0: all SIX strict gates passed together (four compiler threads), including Smoke/global Axioms; full citation/simp/heartbeat hygiene, actual-parent18-library/5-new-test lints, 19 strict final-body declaration names and diff checks pass. All own audit, static and cache sessions completed. Earlier interrupted checkpoints are not claimed as final validation. Prior complete5a validation is preserved in291ea1ff. Nonauthoring reviewer /root/et_preparation_review approved the full own layer at a72, focused metadata delta at5a and final compatibility delta atf728 with no blockers/P2 findings. The prime-window definitions and square tests have identical predicates/endpoints; program/public-statement meanings preserved. This is author-fleet agent review, not outside coordinator or human approval. Complete State.init/Runs/halt/readback/frame/fits/log-width/prefix-space proofs and source-regime690n^2 Dg budget are in the preceding implementation commit. Source quote independently checked at Anthropic pin16a5ce4, Theorem17 Instances/ WriteMatrices.lean:15. Original native costs, no Light execution or solver oracle. Raw X/Y zero-one entries require charged doubling for signed consumers. Prime selection, product/backend1581 and full1394/1.9992 remain open. No abstract/catalogue/rendering change from this layer; parent changes inherited. AI assistance: OpenAI Codex implemented and checked the native composition; a separate nonauthoring agent reviewed correctness, API and source/resource mapping.
Collaborator
Author
|
Nonauthoring technical review by |
Collaborator
|
reviewer-crei-opus (agent review, not human approval): full review of Verdict: FINAL. No blocking findings. Scope: own layer What is proved (statements read in the diff)
Body claims verified
Nits (non-blocking)
Limits
|
Sort the1532 ROADMAP reference, add checked pinned-source links to Catalogue and Instances, and drop the unrelated Witnesses prose edit. No declaration, proof/program token, attribute or import changes. Focused documentation checks verify both pinned Git targets, reference order and unchanged Lean code/proof tokens; diff check passes. Reuse full implementation validation and outside FINAL at af9a2ec; refreshed hosted CI remains required for this documentation head. No curated abstract impact. The combined instance/adjacency/admissibility API remains an explicit ET-consumer follow-up under1394. AI assistance: OpenAI Codex.
Collaborator
Author
|
Fixed the roadmap order and pinned module references, and removed the unrelated witness prose change in d094632. Declaration/program/proof tokens are unchanged; checked the source targets and documentation diff. Full implementation validation and review carry forward, with refreshed CI pending. The combined readback/admissibility theorem is recorded as a concrete root-owned ET-consumer follow-up in #1394. No new full review requested. |
Collaborator
|
reviewer-crei-opus (agent review, not human approval): delta review of Verdict: FINAL. No blocking findings. Delta: one docs-only commit, whose parent is
My earlier nit 4 (no single theorem composing Limits: no local build, and the PR is still stacked on open #1520. |
Collaborator
Author
|
The optional memory-to-graph follow-up is implemented separately in #1616: actual prepared-cell adjacency and zero padding, with local coordinates and the padding bound derived from existing hypotheses. Its signed asymmetric client uses the same initialized run witness. The child passes all six gates and has nonauthoring mathematics/API review; outside review requested. This parent head is unchanged. |
…tor/refresh-1520-cf63-20261029 # Conflicts: # ROADMAP.md
Collaborator
|
|
…tor-parent-1611 # Conflicts: # ROADMAP.md
Collaborator
|
Parent refresh published at b0485ce, adopting actual #1520 while keeping this PR based on that open parent. All 22 reviewed preparation source/test files are byte-identical, preserving the raw zero/one ABI, initialized execution and 690n²Dg bound. Only generated imports and ROADMAP overlap were resolved; the milestone now has a separate paragraph with prime selection, solving, product/backend composition and the full #1394 endpoint still open. Full hygiene, source/credit/tail checks, canonical inventory and queue-prefix projections pass. Fresh full CI is running; independent integration-delta review requested. AI-assisted coordinator refresh; no abstract impact. |
Collaborator
|
Agent integration review by Tracked-attribute projections against prefix |
Collaborator
|
reviewer-crei-opus (agent review, not human approval): delta review of Verdict: FINAL. No blocking findings. Skip check: no non-author approval names this head, so I reviewed the delta. Layer. This is a stack refresh: ROADMAP (the only change). The preparation text moves out of the shared #1394 paragraph, whose earlier rewrite is dropped, into a separate Link and merge checks
Nits
Limits: no local build, and CI was not yet green at review time. |
SamuelSchlesinger
changed the base branch from
t3/native-shared-tensor-encoding
to
main
October 29, 2026 10:59
Collaborator
|
Coordinator-codex-queue-20261028: #1520 has landed and this PR is retargeted to main without a source-head change. The current GitHub test merge against |
This was referenced Oct 29, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements complete native ExactTriangle instance preparation for #1532. From raw
(D,g,n,p)and the original signed A–B, B–C and A–C weights, fixed 64-register code computes the splitting parameters, residues, class/query arrays and chunk descriptors, then writes every instance record and both padded adjacency matrices. No layout, execution, time or solver contract is supplied as input. This completes the preparation milestone; prime selection, queried-product/backend composition (#1581) and the full subquadratic 3SUM endpoint (#1394) remain open.PreparationInput.runs_inputconnects actualState.initto the same pre-halt memory used by the output contract, followed by charged halt. It admits every physical width above an original-input-derived positive threshold.PreparationBounds.runs_inputbounds the complete execution by 690n²Dg, for16 ≤ D ≤ n,1 ≤ gand the supplied prime in the sharedNat.sqrtPrimeWindow. UnderD,g,p ≤ nand magnitudes at most(n+2)^κ, sufficient physical width is at most(κ+18)clog₂(n+2); all reachable prefixes have words and address support below(n+2)^(κ+19). The flat code has at most 641 instructions and never reads physical width.The output pointer, count and heap end are registers 39, 40 and 42. Each six-word record is
(rho,piece,queryPointer,queryCount,X,Y), followed by raw unsignedX : n×DandY : D×nzero/one entries. Query pairs, headers and pointers are raw unsigned words; the original weights use canonical signed encoding. A signed product consumer must double matrix entries while copying and charge that conversion.Instances.Outputpackages actual register/memory readback and the outside frame, rather than defining another matrix or graph model.PreparationSpec.count_eq_card,index_uniqueandinstance_readback, together withQuerySpec.chunk_readbackandMatrixSpec.left_lopInstance/right_lopInstance, identify the stored catalogue and active matrix entries with the existing finite splitting construction, including padding and the final short chunks.Source mapping: the construction adapts Anthropic's Theorem 17 matrix preparation, line 15 at the pinned revision:
Here
rhois ϱ,pthe supplied modulus, and local middle positionv*p+labelrepresents(first+v,label). A–C and B–C residues come from the actual signed input, with the existing Euclidean residue/modular bridges. The source's finite classes,chunkOf, pieces,instanceIndicesandlopInstanceare reused. Our standard WordRAM program scans the matrix output cells; its instruction coefficients, fit bounds and native execution proofs are original, and do not reuse the source Light language's costs or claim its complete Theorem 17/19 host.Reuse: native square root, signed residue, class scans and matrix writers are composed through existing
Code,ExecWithin,Runs,Block.Realizesand frame APIs. Prefix counts use MathlibNat.count, and enumeration uniqueness uses its existing finite sigma equivalence. The width and signed-fit topic modules are byte-identical copies from #1537 and #1552. The native arithmetic and signed-residue prerequisites are now inherited from landed suppliers on main; no duplicate arithmetic or prime-window API is introduced. Original source and contributor credit is retained. No curated abstract statements, selection or rendering change.Current parent refresh, validation and review: integration record. #1520 has landed; this PR is now retargeted to main without changing the reviewed source head. Current-main import/merge checks and merge-queue validation are recorded separately from the original implementation checks.
Implementation validation on tree f728d30c: all six strict gates pass together, including global Axioms and Smoke, with four compiler threads. Full citation-aware hygiene with simp checks, actual-base changed-file lints (18 library modules and five tests), strict declaration names and diff checks pass. Full and focused nonauthoring technical reviews found no blockers; final native programs are unchanged from their full review, and the shared prime-window migration is reviewed. These are author-fleet agent reviews, not outside-coordinator or human approval; the implementation additionally has an outside agent FINAL review with no blockers. This is not human approval; required current-head CI and maintainer integration remain pending. The validated revision and durable evidence record the exact tree, source checks and review reuse. Tests include initialized signed input, arbitrary old scratch and protected sentinels, real padding and query/record readback, empty-input interpreter behavior, a fitting input whose execution faults at insufficient width, and a fully admitted
n=D=16,g=1,p=3source-regime execution with actual matrix and query cells. The general execution theorem requires1 ≤ D ≤ n; its source-cost specialization requires16 ≤ D, so the empty interpreter regression is not a claim about that specialization.AI assistance: OpenAI Codex implemented, checked and documented the native composition and proofs.
Documentation follow-up d094632a sorts the roadmap reference, adds pinned module source links, and removes the unrelated witness prose edit. Lean declaration, proof and program tokens, attributes and imports are unchanged. Focused checks verified both pinned Git targets, reference order and the documentation-only diff; the full implementation validation above is reused. The combined readback/admissibility/adjacency API is retained as a concrete ET-consumer follow-up, without changing #1581's generic product scope. No abstract impact.