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.