ACGN v2.17

ACGN v2.17

Assurance-only release completing five bounded certificate-record and
retained-source binding tasks. Production canonicalization, repair distances,
rewards, certificate semantics and experimental runners are unchanged.

Repaired Scope

• P3-04: complete 17-field law records and independent registry reconstruction, with actual KERNEL verifier observations.
• P3-05: complete flat source trees, splice ledgers and application traces.
• P3-06: ordered container inputs, outputs and fibers, preserving Seq order, Bag multiplicity and Set quotienting.
• P3-12: canonical wire grammar, Java UTF-16 table ordering and content-ID preimages.
• A2-12: deterministic phase/child occurrence paths and retained-source content/provenance bindings.

The package supplies 85 model theorems, including general structural
contracts and a Unicode boundary witness, plus 538 generated Lean replay
propositions over 700 Java observations. It checks 96 Lean negatives
and 54 compiler-resolved source controls in each of two isolated builds.
All 1,106 deterministic artifacts matched in the completed local run.

The shared suite passed all 50 Java entry points, the distance-artifact
regeneration smoke test, and the independent producer/verifier harness.
There are 75 new Python orchestration/encoder tests. Independent bounded
reviews cover the harness and both semantic areas; their reports and corrective
addendum are retained with the failed first integration attempt.

The matrix now reports 112 ready requirements and 105 diagnostics.
PROVED/DIRECT means general model contracts with bounded direct conformance,
not universal Java/parser refinement or full artifact closure. SHA-256 and
collision resistance remain trusted; encoded-string or hash injectivity is
not asserted. No new rewrite law or theory authority is admitted.

Final Verification

Packaging/tag commit: 1e2667351532b0c632166fa21ae5fbc7308a8fe7.

Exact-commit Actions: https://github.com/AlexandervonWu/ACGN/actions/runs/34330242825

The extracted release archive returned VERIFIED, with all five frozen
claims passing, zero unresolved claims, two successful clean builds, and
identical deterministic artifacts. Final closure:
fifth-five-v1-c43c4ccf1e7e6251; input root:
c43c4ccf1e7e625118f2141b605dd41bf4b36cccaf6bf53dfb825365767e654f.

All five exact-commit Actions jobs passed. The downloaded fifth-five CI
report is also VERIFIED and has the same input manifest and root hash as
the extracted archive. The fourth-five CI replay separately returned VERIFIED
with two deterministic clean builds (root
e61c965e1e9cd4d4866d7276f0c650b99a453e5a294e26f56ab15fd38a07396a).
Final reports, input manifests, build ledgers and raw logs are retained in
the verification receipt archive attached below.

The prepackaging report retains its own input root. A corrected KERNEL-level
matrix label and trailing-whitespace cleanup changed the packaging inputs;
the final checks regenerate evidence rather than inherit an earlier VERIFIED
status across that change.

Preserved Experimental Provenance

All 898 existing classes in the v2.16 experimental JAR match the fresh
build byte-for-byte. This release changes assurance sources, tests and
documentation only. No full-corpus rerun was needed or is claimed.

• Full-corpus source: 8ad5fead39b687d2cadc79b01ac27743c1ece990.
• Full-corpus publication run: db9f89bf-0965-4d74-8080-d9191d5f1aec.
• All 5,808 imported outputs, empirical trees, historical manifests and the original full-corpus JAR remain unchanged.
• Separate v2.16 validation run: 659e248c-d3d6-4a2b-8d99-67a0ebcf9eb4, source 8feab00f9190482af6a25334af5b2716653f8ac9, with 29 successful sampled checks.

The attached JAR is that existing v2.16 validation JAR, not a rebuild and
not the JAR that produced the preserved full-corpus measurements. The new
assurance source, proofs, tests and evidence are supplied in the archive.

Certificate coverage remains bounded and fixture-scoped:
1 VERIFIED, 2 UNCHECKABLE, 0 REJECTED. All 31 trusted-pin checks pass, and
the parsed PAIR retains two distinct source hashes. Existing test authority
does not confer general production or corpus-wide certification.

Assets

• acgn-experiments.jar: 2,549,918 bytes, SHA-256 67e7dd088ef864a9170178e6b6c963a2c339836fa88b25cffe8e20788714f04a.
• acgn-v2.17-assurance.tar.gz: SHA-256 9f8cb0afe7c3622c7dad738166209ece9c927d3337ba9bbc6e8502c396ec98c2.
• acgn-v2.17-verification.tar.gz: SHA-256 7da96e50e640bdfbb003834b04583e03bb2fdeddca4db5cae3ad7aae5c43c072.
• SHA256SUMS: run sha256sum -c SHA256SUMS to verify all three assets.

The assurance archive includes tagged source, local libraries, proofs,
bounded runners, documentation and the separate validation publication.
It excludes the full corpus, historical empirical trees and frontend.
Its closure runner supports extracted archives; the standalone producer
provenance harness requires a Git checkout. Reviewers using the full repository
must run git lfs pull for the large experimental JSON files.

Details: release record,
bounded verification,
and incidents.

ACGN v2.16

ACGN v2.16

Capability validation now selects bounded temporal solving for temporal operators hidden inside predicate or function bodies. The checker exposes temporal mode with Q and after true only when necessary; source predicates, signatures, scopes and rewrite rules are unchanged. Errors and inconclusive results fail the check.

Validation

• Refreshed deterministic sample: 29 checks, 0 counterexamples, 0 errors, 0 inconclusive results. Eight commands use temporal solving, including the six formerly inconclusive cases at scope 4 and trace bounds 1 through 10.
• 95 regression assertions pass in each of two fresh builds. Five constructive Lean guard theorems and the existing six temporal duality proofs compile. Java classes, Lean objects and sample CSVs agree across those builds.
• The bounded Java suite and independent certificate harness pass. The release archive is also extracted and checked; the exact-commit CI includes the two-clean-build obligation suites.
• Exact-commit CI: https://github.com/AlexandervonWu/ACGN/actions/runs/34313157828

All four exact-commit CI jobs passed. Both the extracted archive and hosted
CI report the five-claim bounded closure fourth-five-v1-7235b6999a1a91d8
as VERIFIED, with two passing clean builds and identical artifacts under
input root 7235b6999a1a91d8c0f609e2c0ca676dd5f2bc6331d1ab8acce3cb4806cdb361.
This regenerates evidence for the current source; it does not transfer the
older closure report's status across an input change.

These are finite-scope checks and stated Lean contracts, not a universal soundness proof. The dataset identity covers 5,500 generated models; the refreshed solver sample is 29 cases, not all 5,500.

Provenance

• Final packaging/tag commit: c9475b6e5d5ef2508dc312b667d7bf33783cee9e.
• Clean validation source commit: 8feab00f9190482af6a25334af5b2716653f8ac9.
• Validation run: 659e248c-d3d6-4a2b-8d99-67a0ebcf9eb4, one worker, 1 GiB heap, no reward evaluation. Its manifest binds all 21 generated outputs.
• Unchanged full-corpus result-producing source: 8ad5fead39b687d2cadc79b01ac27743c1ece990.
• Unchanged full-corpus publication run: db9f89bf-0965-4d74-8080-d9191d5f1aec. All 5,808 imported files, historical manifests and the original result-producing JAR remain unchanged. No new four-stage corpus experiment is claimed.

The attached JAR is the frozen JAR used for the new validation and contains the repaired checker. It is not the JAR that produced the preserved full-corpus results. Historical validation reports remain attached to their original manifests; the new report is published separately under the validation run.

Downloads

• acgn-experiments.jar: 2,549,918 bytes; SHA-256 67e7dd088ef864a9170178e6b6c963a2c339836fa88b25cffe8e20788714f04a.
• acgn-v2.16-assurance.tar.gz: SHA-256 c81de3b4410e6e9522665071878cbae20198d6f7ea085249ab762bfcdf658019.
• SHA256SUMS: verify both assets with sha256sum -c SHA256SUMS.

The assurance archive contains the tagged source, libraries, Lean proofs, bounded runners, documentation and new validation publication. It excludes the full corpus, historical empirical trees and frontend. Its bounded closure runner supports extracted archives; the producer certificate-provenance harness requires a Git checkout. For the full repository checkout, reviewers must run git lfs pull to obtain the large experimental JSON files.

Remaining Scope and Next Work

Certificate coverage remains bounded and fixture-scoped: 1 VERIFIED, 2 UNCHECKABLE, 0 REJECTED. Test-only theory authority is unchanged. The broader assurance matrix remains 107 ready requirements and 111 diagnostics, and is incomplete; this validation repair adds no new blanket closure.

The next five proposed bounded obligations are P3-04 (complete law-record decoding), P3-05 (flat-record decoding/replay), P3-06 (container-record reconstruction), P3-12 (canonical wire tables and content-ID preimages), and A2-12 (phase/occurrence path and source-content commitments).

Details: release documentation, temporal incident and proofs, and next bounded tasks.

ACGN v2.15

ACGN v2.15

Closes the five bounded correspondence repairs P2-20, A2-07, A2-11, P2-18 and
P3-03. The work repaired three concrete certificate production/replay defects:
source-profile version drift, recursive splice ordering, and missing exact
intermediate types in dependent-chain exports. No new rewrite family is added.

The five-claim closure is VERIFIED under its declared trust boundary: two clean
builds, 1,076 identical artifacts per build, 66 general Lean theorems, 9,128
replay propositions/blocks, and all registered rejection checks passing.
The assurance archive also reproduces the same closure after extraction.
The broader Java suite includes 45 test entry points. Certificate census:
1 verified, 2 uncheckable, 0 rejected, with distinct parsed-source PAIR hashes
and unchanged fixture-scoped authority. This is bounded evidence, not complete
Java/parser refinement; the full matrix retains 111 diagnostics (107 ready requirements).

Fresh Full-Corpus Run

All four stages were rerun before publication, strictly serially, with 16 workers,
an 8 GiB heap, reward pool 100, and one unchanged experiment JAR:

• 66,080 files; 61,598 eligible successes; 4,482 AST-identical skips.
• 42,386 incorrect predicates ranked and rewarded; no parse, ranking or reward failures.
• Zero incorrect nearest-truth zeroes in both Fast Rewrite and Certificate-Integrated IR.
• Seven full-corpus ablation arms, zero failures or incorrect merges.
• 4,088 claimed-equal pairs checked with bounded Alloy, no counterexamples/errors.
• 5,500/5,500 capabilities captured by slotted, Fast Rewrite and Certificate-Integrated IR.
• Six temporal capability solver checks remain explicitly inconclusive.

The 5,808 imported stage files pass their manifest hashes. Distance and equality
headline results are reproduced; runtime/memory have been remeasured. Rewards
are available for this run and remain finite sampled evidence, not semantic proofs.

Exact Provenance

• Result-producing source: 8ad5fead39b687d2cadc79b01ac27743c1ece990 (clean).
• Publication run: db9f89bf-0965-4d74-8080-d9191d5f1aec.
• Packaging/tag commit: 5eba7ca15e29466e9ba813efb50c908f79f07cd9.
• Closure: fourth-five-v1-58c1aae07b2d37dc.
• Closure input root: 58c1aae07b2d37dc98459c7c9989cb942b0845ec1fce579b8ca19836b16a133b.
• Exact-commit Actions.
• Repair, evidence and limits.
• Publication provenance.

Reviewers must run git lfs pull in the full checkout. The attached experiment
JAR is copied unchanged from the new completed run, not rebuilt from the packaging
commit. Earlier archived JARs/manifests remain unchanged. The assurance archive
contains source, libraries, proofs, runners and retained evidence; use the full
checkout for corpus, empirical result trees and frontend.

Verify both attached assets with sha256sum -c SHA256SUMS.

• acgn-experiments.jar: 2,540,041 bytes; SHA-256 a053e40e64faa2ecffb0f4999b57aa661eae51933d6daf93a95d973144a71abf.
• acgn-v2.15-assurance.tar.gz: SHA-256 358f34e10fd3624015ebff5fa5381fdd630aeeb7cfc347f325b280d12f14c3c0.

ACGN v2.14

ACGN v2.14

Five more bounded assurance obligations are repaired: P1-06, P1-09,
P1-16, P2-19, and A2-04. These cover independent CALL arity/authority,
executable occurrence nonreuse, ordered and nested CALL representation,
complete registry/profile binding, and arbitrary-length guarded relational JOIN.

Evidence

• Five frozen claims VERIFIED in two clean builds, with 1,053 identical artifacts each.
• 74 new general Lean theorems, 166 imported theorem audits, and 1,414 generated replay propositions.
• 10,628 Java observations and 18,800 assertions across the three new tests.
• All 28 Lean negative controls and 26 source-mutation controls reject for their registered reasons in each build.
• 33 runner and 34 area encoder tests pass; independent bounded reviews and failed-candidate records are retained.
• The full matrix remains INCOMPLETE: 102 ready requirements and 118 diagnostics.
• Certificate coverage remains bounded and fixture-scoped: 1 verified, 2 uncheckable, 0 rejected.

These results are general model proofs plus bounded direct conformance under
an explicit trusted computing base, not universal Java/parser refinement or
corpus-wide certification. Original requirement statements/hashes are unchanged.
P1-19's independent source-occurrence authority and A-01's complete typed
contract registry remain open.

Provenance And Assets

• Packaging/tag commit: 91825cff2b7c4b460cb5bc6160bf2df4ff95b089.
• Exact-commit Actions: https://github.com/AlexandervonWu/ACGN/actions/runs/34247620652
• Frozen assurance input root: 4d63586625ff6c0a4f5bc923ed19ecbb377b88d2c768ea504a39b965f9393003.
• Result-producing source: fbd9b1497a9036c55780da777f56581bc1c6bcec.
• Publication run: df4d8d4c-6265-4fe7-88d5-3aceee60398b.
• acgn-experiments.jar is the existing, unrecompiled v2.11 JAR: 2,292,989 bytes; SHA-256 361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807.
• acgn-v2.14-assurance.tar.gz packages this commit's source, local libraries, proofs, bounded runners, documentation, and evidence. It excludes the corpus, result trees, and frontend.
• SHA256SUMS binds both attached assets. Verify it before use.

Production canonicalization, repair metrics, certificate semantics/authority,
the prior assurance packages, and all empirical trees remain unchanged. The
snapshot verifier checks the same 5,808 files. Rewards and correlations remain
those of the v2.11 pool-100 run; no experiments were rerun for v2.14.
Reviewers using the full repository must run git lfs pull before reading
the large experimental JSON files.

Reproduce

From the checkout or extracted assurance archive, with Java 17, Python 3,
and locally installed Lean 4.33.0:

python3 -B scripts/run_third_obligation_repairs.py /tmp/acgn-v214-third-five
python3 -B scripts/report_obligation_repairs.py --output /tmp/acgn-v214-obligations

Use fresh output directories outside the source tree. The third-five runner
creates two isolated builds, including deterministic TEST_ONLY Git provenance;
it supports an extracted archive without .git. The older container and
Java-Lean refinement runners still require a Git checkout.

The attached assurance archive was extracted and rerun locally without .git:
both clean builds VERIFIED all five claims at the same frozen input root.

Next Five Candidates

1. P2-20: recursive flattening iff exact typed associativity evidence exists.
2. A2-07: independent exact leaf type/view proofs and complete field controls.
3. A2-11: complete dependent-chain index reconstruction across writer/verifier.
4. P2-18: exact permutation, quotient, splice, and endpoint witness indices.
5. P3-03: profile serialization and independent five-field fingerprint replay.

These are proposed work, not additional repairs completed in this release.
See docs/obligation-repair/third-five/README.md and
docs/obligation-repair/next-candidates-v2.14.md for evidence and boundaries.

ACGN v2.13

ACGN v2.13

An assurance-only continuation of v2.12, covering the next five obligations:

• P2-06: exact flat element/result typing through a shared substitution.
• A2-01: ordered dependent JOIN/ARROW sequence construction and replay.
• A2-02: chain length and operand multiplicity preservation.
• P1-08: arbitrary-arity CALL validation without neighboring-visit fallback.
• P1-05: source argument order through the retained CALL boundaries.

Verified Evidence

The frozen five-claim package passed two clean builds with 1,026 identical artifacts per build, 48 general Lean theorems, 2,636 generated propositions, and all 21 required rejection controls per build. The three new Java tests execute 66,872 assertions per build; 33 runner and seven encoding unit tests pass. Independent bounded reviews and their repaired findings are retained in docs/obligation-repair/next-five/.

Input root: c627da30a64e66506a1dcb777fd94e9dcbee7e2b5a64ad7bcb7e37557d360da0.

A fresh replay from the extracted release bundle, without a Git checkout or a default elan toolchain, also passed both builds. All 1,026 artifact hashes per build matched the repository run.

The full bounded Java and standalone producer/verifier harnesses pass. The matrix now has 97 ready requirements and 123 diagnostics, compared with 92 and 128 in v2.12. These are proved models with bounded direct conformance, not whole-parser or whole-JVM refinement. The global matrix remains incomplete.

The standard certificate census remains 1 VERIFIED, 2 UNCHECKABLE, 0 REJECTED. Certificate coverage is bounded and fixture-scoped. Parsed local chain observations are distinct from the separate TEST_ONLY FULL-verifier fixtures; unsupported parsed exports are not relabeled certified.

Provenance

• Final packaging/tag commit: 892e001ee9f81fc5cf9ac2f4984c4b8be474e18c.
• Exact-commit CI: https://github.com/AlexandervonWu/ACGN/actions/runs/34159720543
• Result-producing source commit: fbd9b1497a9036c55780da777f56581bc1c6bcec.
• Publication run: df4d8d4c-6265-4fe7-88d5-3aceee60398b.
• Production Java, experimental trees, certificate authority, and the archived experiment JAR are unchanged. All 5,808 manifest-bound publication outputs verify.
• Existing reward results and correlations remain those of the v2.11 run with pool size 100; no experiments were rerun for this assurance release.

Reviewers using the full repository must run git lfs pull before checking the large empirical JSON files.

Reproduction

The source/proof bundle contains the bounded runners and dependencies, not the corpus/results or frontend. From the extracted bundle, with Java 17, Python 3, and installed Lean 4.33.0:

python3 -B scripts/run_next_obligation_repairs.py /tmp/acgn-v213-next-five

Use a fresh output directory. The new runner creates local deterministic TEST_ONLY Git provenance for its isolated verification snapshots, not publication authority. The two older container/refinement runners still require a Git checkout, as documented.

Assets

acgn-experiments.jar is the existing, unrecompiled v2.11 experiment JAR (2,292,989 bytes). acgn-v2.13-assurance.tar.gz is the tagged assurance source and evidence package (58,103,083 bytes). SHA256SUMS binds both assets.

361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807  acgn-experiments.jar
e2ea9ab0203f5f509c90f098cdaf32653f27cbe2f839af85c79e67e1a70f7b5c  acgn-v2.13-assurance.tar.gz
bebd1d17aaa2de1dd423ac4a9f76e26e7383b552eb065c88a72ed6700ac18549  SHA256SUMS

ACGN v2.12

ACGN v2.12

An assurance and reproducibility update. This release does not change the
production canonicalizer, distance metric, rewarder, or certificate semantics,
and does not claim a new experimental run.

New assurance work

• Finite Java-to-Lean container replay and compiler-extracted Boolean
  smart-construction correspondence, each with explicit scope and retained
  historical input hashes.
• Five bounded ledger gaps repaired: P2-02 (nominal policy fields), A2-06
  (JOIN interior guard), P2-05 (single root port), P1-10 (zero-argument CALL),
  and P5-15 (built-in identity and empty cardinality).
• Two identical clean builds of the five-claim package: 77 general and 93
  generated Lean theorems, 370,365 assertions in the five new Java tests, and
  17 required rejection controls per build.
• Explicit A-01 rejection when authoritative decomposition evidence is
  missing. The full ledger remains INCOMPLETE: 92 ready requirements and
  128 diagnostics (127 original diagnostics plus the exposed A-01 blocker).

The full bounded Java suite and standalone producer/verifier harness passed.
Certificate coverage remains bounded and fixture-scoped: 1 VERIFIED,
2 UNCHECKABLE, 0 REJECTED. These results do not establish whole-parser,
whole-JVM, or whole-corpus semantic verification.

Provenance

• Final packaging/tag commit: 59045ead958b5f8397100c39ab68557a3cb05399
• Exact-commit Actions: https://github.com/AlexandervonWu/ACGN/actions/runs/34155260001
• Five-claim closure input root:
  1e34a74d3b5be4e39af665571123907e27950b24dabd43a4b63d5594752c5825
• Unchanged result-producing source commit:
  fbd9b1497a9036c55780da777f56581bc1c6bcec
• Unchanged clean publication run:
  df4d8d4c-6265-4fe7-88d5-3aceee60398b

All 5,808 manifest-bound imported files verified unchanged. The dataset and
empirical result trees are unchanged from v2.11. Reviewers must run
git lfs pull when using the full repository. Rewards and correlations remain
those of the v2.11 clean run with pool size 100; they were not recomputed here.

Assets

• acgn-experiments.jar: the unrecompiled, byte-identical archived v2.11 JAR,
  2,292,989 bytes; SHA-256
  361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807.
• acgn-v2.12-assurance.tar.gz: tagged source, dependencies, proofs,
  bounded-check scripts, and evidence; 50,772,717 bytes; SHA-256
  e5a5880f98248acd67616e5c62af41c6ce48ca324bfcc26f8ae027d6d61ae938.
  This is an assurance package, excluding the corpus/results and frontend.
  Its extracted files match the verified five-claim input manifest exactly.
• SHA256SUMS: checksums for both assets; SHA-256
  f6aa68717fba3d1b04a0c77819306de600c486ddd5504f7546a2bfda3b4e4dcf.

Publication CI caught an isolated-working-directory toolchain-selection bug
in the new proof runner. The release fixes it by explicitly selecting and
checking Lean 4.33.0 in both proof directories, retains the earlier evidence
as superseded, and includes a fresh two-build replay. No tag was published
from either failed or cancelled candidate. The two older refinement/container
runners require a Git checkout for Git HEAD provenance; the release guide
distinguishes those commands from the archive-compatible five-claim runner.

See the release guide
and bounded repair report
for reproduction commands, proof boundaries, and retained evidence.

Recommended next obligations

All of these remain PARTIAL/DIRECT; this release does not mark them proved.

1. P2-06: exact flat element/result type equality through instantiation and
   substitution, reusing the single-root-port extractor.
2. A2-01: general left-to-right JOIN/ARROW chain construction and replay.
3. A2-02: general chain length and duplicate-occurrence count preservation,
   sharing A2-01's traversal model but retaining a separate obligation.
4. P1-08: executable CALL validation at arbitrary arity, including proof
   that the CALL path cannot use another visit as a fallback.
5. P1-05: argument-order preservation from parser occurrences through
   retained certification-source IR and ordered certified endpoints.

P2-06 is the recommended first target. A-01 remains a specification blocker:
its missing authoritative parent contracts cannot be supplied by more examples
or an otherwise well-formed theorem-name registry.

ACGN v2.11

ACGN v2.11

This release publishes the August 29, 2026 clean full-corpus replay after
repairing the Fast Rewrite IR field-ownership and inherited-temporal alpha
alignment boundaries. The Certificate-Integrated pathway and its fail-closed
semantic boundary remain intact.

Provenance

• Result-producing source commit: fbd9b1497a9036c55780da777f56581bc1c6bcec
• Clean publication run: df4d8d4c-6265-4fe7-88d5-3aceee60398b
• Final packaging and tag commit: 63f3b8c2931202e9b3582a8802c558725a67ac26
• Dataset: 66,080 Alloy files; 61,598 eligible AST-different pairs
• Imported manifest-bound stage outputs: 5,808 files
• Configuration: Java 17.0.20, 16 workers, 8 GiB heap, reward pool 100
• Exact-commit Actions run: https://github.com/AlexandervonWu/ACGN/actions/runs/33281721348

Reviewers must run git lfs pull before verifying the two large JSON result
files. Run ./scripts/verify_imported_publication_snapshot.sh to check every
imported stage artifact against the archived run manifest.

Headline results

• Paired evaluation: 61,598 successes, 4,482 AST-identical skips, 0 failures,
  and 0 incorrect zeroes under either canonical path.
• Augmented evaluation: all 42,386 incorrect predicates ranked and rewarded,
  with 0 preparation, ranking, or reward failures and 0 incorrect-to-truth
  zeroes under both Fast Rewrite and Certificate-Integrated distance.
• Seven-arm ablation: all 431,186 eligible arm rows succeeded. The
  Certificate-Integrated IR certified 4,088 CORRECT zeroes, retained all
  4,074 Fast Rewrite IR zeroes, and added 14.
• Bounded natural-corpus semantic replay: 4,088 unique claims, 0
  counterexamples, and 0 errors; four targeted negative controls remained
  unmerged.
• Capability matrix: slotted e-graph, Fast Rewrite IR, and
  Certificate-Integrated IR each recovered 5,500/5,500 generated pairs.
• Rewards and reward correlations are present. Both rewarded stages used pool
  size 100 and reported 0 reward failures.

Repair in this release

The preceding snapshot exposed ten Fast Rewrite-only incorrect-to-truth
zeroes. Nine erased the owner coordinate of same-named fields, and one allowed
inconsistent alpha mappings for an inherited binder across temporal phases.
Fast Rewrite now retains field-owner identity and minimizes one coherent
inherited-temporal mapping. The full replay reduces both incorrect-zero counts
to zero while preserving all previously observed paired CORRECT Fast Rewrite
zeroes. The Certificate-Integrated pathway was not broadened by this repair.

Certificate and assurance boundary

Certificate coverage remains bounded and fixture-scoped. The exported
certificate census is 1 VERIFIED, 2 UNCHECKABLE, and 0 REJECTED; it is
not a corpus-wide proof of Alloy equivalence. The checked-in Section 3
assurance record remains INCOMPLETE while its documented metatheoretical and
refinement obligations remain open.

Assets

• acgn-experiments.jar: 2,292,989 bytes; SHA-256
  361b33ef56f6ccb1089a7a6fdda2a92bf621e501166c5a1c73330a0cc1686807
• SHA256SUMS: SHA-256
  798a0dac47d0a186ca91eab6368adfda63434538895db660dbdc431a25d4a69c

The JAR is the byte-identical archived experiment artifact from the clean run;
it was not rebuilt for this release.

ACGN v2.1

ACGN v2.1

This release publishes the August 28, 2026 clean full-corpus replay and the
certified Set-carrier repair that closes the targeted capability matrix.

Provenance

• Result-producing source commit: 88363ea23728329948ccc9d5cdad690cc5787ca5
• Clean publication run: 57f5a2d8-f501-494d-81d5-b3f1396dbe18
• Final packaging and tag commit: 431ca3229e9f5e7464bf86521659b0caa7b9ca17
• Dataset: 66,080 Alloy files; 61,598 eligible AST-different pairs
• Imported manifest-bound stage outputs: 5,808 files
• Configuration: Java 17.0.20, 16 workers, 8 GiB heap, reward pool 100

Reviewers must run git lfs pull before verifying the two large JSON result
files. Run ./scripts/verify_imported_publication_snapshot.sh to check every
imported stage artifact against the archived run manifest.

Headline results

• Paired evaluation: 61,598 successes, 4,482 AST-identical skips, 0 failures,
  and 0 incorrect certificate-integrated zeroes.
• Augmented evaluation: all 42,386 incorrect predicates ranked and rewarded,
  with 0 preparation, ranking, or reward failures and 0 certified
  incorrect-to-truth zeroes.
• Seven-arm ablation: all 431,186 eligible arm rows succeeded; the
  Certificate-Integrated IR found 4,088 CORRECT zeroes and retained every
  Fast Rewrite IR zero.
• Bounded natural-corpus semantic replay: 4,088 unique claims, 0
  counterexamples, 0 errors; four targeted negative controls remained
  unmerged.
• Functionality matrix: slotted e-graph, Fast Rewrite IR, and
  Certificate-Integrated IR each recovered 5,500/5,500 generated pairs.
• Rewards and reward correlations are present; both rewarded stages used pool
  size 100 and reported 0 reward failures.

Certificate and assurance boundary

Certificate coverage remains bounded and fixture-scoped. The exported
certificate census is 1 VERIFIED, 2 UNCHECKABLE, and 0 REJECTED; it is
not a corpus-wide proof of Alloy equivalence.

The bounded Section 3 harness executed 77 steps with 0 failed executable
steps, including every mapped Lean file and the forbidden-token scan. Its
overall assurance state remains honestly INCOMPLETE because 132 declared
metatheoretical and traceability diagnostics remain open. The capability
soundness sample has 0 conclusive non-temporal failures; six temporal checks
remain explicitly inconclusive because this installation has no temporal
backend.

Assets

• acgn-experiments.jar: 2,285,442 bytes; SHA-256
  7b308e3156fbb36dfeda4af52f8ec339132546a0fcabb24129227f41debbad71
• SHA256SUMS: SHA-256
  f33c5e61345f697c3575e69f74af9a0fe1d4581ca16081ec3659c2fa5175c89f

The JAR is the byte-identical archived experiment artifact from the clean run;
it was not rebuilt for this release.

ACGN publication artifact freeze v2

ACGN publication artifact freeze v2

This release freezes the accepted August 27, 2026 full-corpus publication snapshot.

Provenance

• Result-producing source commit: ebce874382c87108a32874149008842a7b0fa528
• Clean publication run: 6000d695-8b5e-4972-b0ea-3d9e55111245
• Final packaging and tag commit: 184dd8c368a6e3d2975bac81e13992bce6e1cf67
• Dataset: 66,080 Alloy files; 61,598 eligible AST-different pairs
• Imported manifest-bound stage outputs: 5,808 files
• Configuration: Java 17.0.20, 16 workers, 8 GiB heap, reward pool 100

Reviewers must run git lfs pull before verifying the two large JSON result files. Use ./scripts/verify_imported_publication_snapshot.sh to check the imported result trees against the archived run manifest.

Headline results

• Paired evaluation: 61,598 successes, 4,482 AST-identical skips, and 0 failures.
• Certificate-Integrated IR: 4,088 AST-different CORRECT zeroes and 0 incorrect paired zeroes.
• Augmented nearest-truth evaluation: 42,386 incorrect predicates, 0 failures, and 0 certified incorrect-to-truth zeroes.
• Fast Rewrite IR retains 10 nearest-truth zeroes as explicitly non-certifying diagnostics.
• Seven-arm ablation: every arm completed all 61,598 eligible pairs with 0 failures and 0 incorrect paired zeroes.
• Bounded natural-corpus semantic checks found no counterexample among the 4,088 claimed-equivalent pair union.
• Capability benchmark: 5,500 generated pairs; slotted recovered 5,500, while both canonical arms recovered 5,492 and agreed pairwise.
• Rewards and reward correlations are available in this clean run; both rewarded stages used pool size 100 and reported 0 reward failures.

Certificate and assurance boundary

Certificate coverage is bounded and fixture-scoped. The exported certificate census remains exactly 1 VERIFIED, 2 UNCHECKABLE, and 0 REJECTED. This is not a corpus-wide proof of Alloy equivalence.

The bounded Section 3 harness executed 62/62 steps successfully, including all mapped Lean files and the forbidden-token scan. Its assurance outcome remains honestly INCOMPLETE because 212 declared traceability obligations are open.

Assets

• acgn-experiments.jar: 2,258,622 bytes; SHA-256 21b721e31b5270c1b5e63bca368eccee9323886fd5c571e6190c296a853abc52
• SHA256SUMS: SHA-256 0de4278fff168e20f0acbc25da91027720fb0e672b1d269211c3dab536ac0e5b

The JAR is the archived run asset and was not rebuilt for this release.

ACGN publication artifact freeze v1

Result-producing source commit: f1bb1607911a4e5a7a0b8527be65148f66cf72d8

Clean publication run: dc368829-9623-4856-8bf1-b655aeaf59e0

Final packaging/tag commit: 8ec25613e81d7b3767947db31c60cc4bbed4074d

After checkout, reviewers must run git lfs pull before verifying the imported snapshot.

Certificate coverage is bounded and fixture-scoped. fixture-empty-theory-v1 is approved only under TEST_ONLY; fixture-parent-path-theory-v1 is approved only under TEST_ONLY_INPUT_SPECIFIC for its single declared right=left ground fixture equation. Neither pin is a general authority for arbitrary producer equations, corpus-wide certification, or production claims.

Certificate census: 1 verified, 2 uncheckable, 0 rejected.

Rewards were disabled in the clean publication run, so reward correlations are unavailable.

Archived assets are the existing result-producing acgn-experiments.jar and its SHA256SUMS; the JAR was not rebuilt for this release.