Astra's audit patches: applied 2026-10-14

Dennis (2026-10-14): apply Astra's patches. Source: coord/patches/astra-audit-public/ (17 patch files, READMEs, validation JSON). All target machines are Claude-owned (coord/claims.tsv, latest line per tm). Nothing under an Astra claim, tools/ or vendor/ was touched. Backups of every original are in the session scratchpad (astra-patches/orig/).

How each patch was handled

• git apply --check against the current files: 11 of 17 applied cleanly. The 6 W4-3-family patches (3 public, 3 header) failed, as expected: PR #17's text was already corrected on 10-13 and merged upstream on 10-14.
• Clean patches were applied as-is. Every resulting file matched Astra's recorded draft sha256 byte for byte (validation JSONs) before the disclosure edit below.
• W4-3 family: reconciled by a 3-way merge (git merge-file), base = the pre-fix originals saved by the 10-13 PR #17 fix (sha 02a8d63c / bb3d65c6 / 2b096112 and the old .v files), theirs = Astra's drafts rebuilt from them (they reproduce Astra's draft hashes 7c9b27be / e8469c12 / 19d0855d), ours = current. Every substantive hunk conflicted because the current text already carries that correction in our own wording. Astra's addendum coord/audits/2026-10-14-pr17-revision-addendum.md confirms each correction is present. The only non-conflicting hunk left in each write-up was the disclosure line. The W4 .v files were not changed (their bytes are upstream).
• Disclosure: Astra's line "... Claude (Anthropic) and GPT-6 Astra (OpenAI)." was replaced everywhere by the house dual line: AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI). tools/writeup_lint.py does not prescribe an exact disclosure form, so the tool was not involved.
• W5-5 .v header: in the comment, Astra's AI assistance: Claude (Anthropic) and GPT-6 Astra (OpenAI). became Formalized with Claude Code (Anthropic, AI-assisted); corrections from an independent audit by GPT-6 Astra (OpenAI). (wrapped over two comment lines). This keeps the formalization statement and uses the house wording. The 4,942,482 -> 4,942,483 iteration fix was applied as written. Side effect, fixed in the fix round below: the .v grew from 2,975 to 2,976 lines, so every line after 25 moved down by one.

Propagation edits outside Astra's patch files: W5-4 README.md and discord.md, W5-3 discord.md and README.md (disclosure only), W5-7 README.md and discord.md, the W4-3b sentence. Each one carries an Astra correction into a sibling text of the same package that held the same wrong statement. The discord drafts' character counts and "same wording as the README" notes were updated to match.

Fresh gate (W5-5)

tools/check_kill.sh --halt on machines/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---.v. It ran one coqc at a time, under ulimit -s unlimited, ulimit -v 8000000 and nice -n 10.

• Result: PASS, exit 0, checked_at 2026-10-14T16:37:56Z, on sha256 5b83f5b1511a76ab796413c74d7789dfe120faeec07f57a4aa07e271cf833f39.
• Compile: 607.1 s, native.
• Assumptions: 0 (closed).
• coqchk: timed out at the 600 s cap. This is advisory under policy A.
• Integrity: the input hash and the framework were unchanged during the run.
• Comment-only: with nested comments stripped, the new file equals the old one (866a5226...27f4). The submission copy is byte-identical.
• Receipt: submission/check_kill.txt, now sha256 ed2c1b24108ede0cc0ec185bc09183ba303e15ac51fcff27bf0ef403fbfa1c01. The old receipt is in the scratchpad.
• status.json kill block: sha256 updated, with previous_sha256 and astra_audit_sha256 set to 866a5226, a header_note, and the new check_kill record. The previous run moved to earlier_runs.
• coord/audits/queue.tsv: the W5-5 row's sha256 is updated, and a note column was added (filled only on that row). The note says that Astra's audit record stays on 866a5226.

Hash changes

The original audited hashes remain Astra's audit record (coord/audits/results.json, reviewed-artifacts.json). The W4 .v hashes (13db03a7, 909abd2a, 6182b097) did not change.

Also changed: W5-5 status.json, coord/audits/queue.tsv (W5-5 row + note column).

Also synced (internal, not public): machines/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---/rocq/test/header.txt (assembly header for the W5-5 .v).

Lint (python3 -B tools/writeup_lint.py)

Every changed proof.md, parent copy and README has 0 errors. One changed file has a lint error: the W5-3 discord.md pasting checklist (item 4, rule checkpoint). It was there before and sits outside the block that gets posted. The fix round below adds its own lint results.

The warnings are preexisting density warnings: the same rule counts as before the patches (#4/#4b 5 dense-paragraph + 3 dense-bullet + 3 inline-formulas; #12 and #12b's parent 28 + 12 + 9; #12b 11 + 6 + 4). The discord.md drafts begin with a pasting checklist for Dennis that trips the linter (W5-3: 1 checkpoint ERROR in checklist item 4; W5-7: 3 warnings). These are preexisting and outside the message block that gets posted.

Fix round after the independent verifier (2026-10-14, 10:12)

The verifier found one blocking issue and six minor ones. No .v file changed in this round. W5-5 stays at 5b83f5b1 with its 16:37:56Z PASS, and the W4 .v files are unchanged. So no new check_kill was needed.

• Blocking, W5-5 line map: fixed (option A, no new gate). The two-line disclosure made the .v 2,976 lines long (it was 2,975), so every line after 25 moved down by one. I checked this two ways: the old file from line 27 on equals the new file from line 28 on, and Definition tm / s751 / halt now sit on lines 35 / 2202 / 2954. Every bound in the ".v map" table went up by one (34-36 -> 35-37, ..., 2202-2953 -> 2203-2954). I also changed "2,975 lines" -> "2,976 lines" in submission/proof.md, in the internal machines//proof.md (with the same table, and its provenance line now names 5b83f5b1), and in submission/README.md. In status.json, kill.lines is now 2976, kill.audited_note covers the 851ca695 -> 866a5226 -> 5b83f5b1 chain, and updated is 2026-10-14. notes.md's "2,975-line .v" is a dated 10-13 record and was left as is.
• W5-4 README, Template sentence: fixed. "a 3-cell lattice that grows at each overflow" -> "whose overflow rule depends on the zone width modulo 3".
• W4-3 family READMEs, older than the PR #17 fix: fixed by rewording them from the merged write-ups. The .v files were not touched.
• W4-3: "every long block is 9 times longer" -> u -> 9u with affine lengths (74844u - 36 -> 673596u - 36). "18 single-block runs with symbolic gaps" -> the 17 runs the proof uses (11 symbolic, m = 3; 6 of block 1 with concrete lengths). The tape is alternating "between two blank ends", and a sweep complements the cells it crosses, so the defect pattern changes only when the head meets a defect.
• W4-3c: the same u -> 9u wording. "Its whole development is kept verbatim" -> "Its simulator and invariant library is kept verbatim". It also gets "between two blank ends".
• W4-3b: "The parent's whole development is kept" -> "The parent's simulator and invariant library is kept". The verifier did not flag this one; I changed it to match W4-3c.
• The three READMEs carry the dual disclosure line now. The W4-3 family discord.md is the record of the message posted on 10-13, so it was not edited (open issue 10).
• #4b proof.md line 144: fixed. "different points of the same contracting map" -> "different orbits of the same affine maps (spectral radius below 1)". This matches the #4 correction. The file now carries the dual disclosure line.
• W5-8b / W5-8c .v comments, reversed map: not changed. They are outside the 17 patches, and the fix needs fresh gates (open issue 9).
• Mailbox: the 094000 message overstated the lint result. It also left out the W5-5 line-map side effect. Follow-up: coord/mailbox/to-astra/20261014-101245-claude-fix-round-hashes.md, with the new hashes and corrected lint wording. It also explains the W5-4 README hash mismatch that Astra reported in 20261014-100839 (the edit from this round). I re-checked the 30 hashes announced in 094000 against the current bytes: 29 match, and the 30th is that W5-4 README.
• Record: open issues 7 and 8 are updated, and 9 and 10 are added. The W5-5 bullet and the lint summary above are corrected.

Backups of the pre-fix-round files are in the session scratchpad (fix2/orig/).

No other file in any submission/ dir carried a copy of these files (checked by sha256 and by searching for the old phrases).

Lint for this round (python3 -B tools/writeup_lint.py): W5-5 submission/proof.md 0/0, W5-5 submission/README.md 0/0, W5-4 README 0/0, W4-3 / W4-3b / W4-3c README 0/0 each, #4b proof.md 0 errors / 9 warnings (the same 9 as before the edit, all preexisting density warnings). The internal W5-5 proof.md is not public. It keeps its 14 preexisting internal-path errors (same count as before) and gains one edit-date warning from its dated provenance line.

Open issues

1. W4-3 family .v headers (merged upstream, unchanged here). All three still say "Formalized with Claude Code (AI-assisted)." Astra's header suggestions name Anthropic and Astra's comment review. The line is accurate but incomplete. A comment-only upstream follow-up is Dennis's call.
2. W4-3b and W4-3c merged headers, map wording. "row q of this machine = parent row phi q, with every target state renamed by phi" is ambiguous. Read literally, it renames the parent's targets, which is the wrong direction. Astra's wording is exact: "mapping both source and target states by phi gives the parent entry". The theorem is unaffected (perm_phi is checked by Coq), and the public write-ups state the map exactly. An upstream follow-up is Dennis's call.
3. PR #17 body (merged) and the local draft family/pr_body.md credit only Claude. Astra asked for its name there too (mailbox 20261014-091339). Editing a merged PR body is a public action, so it is Dennis's call. The draft is left as the record of what was posted.
4. coord/audits/queue.tsv W4 rows. They still carry the pre-fix shas (64d69ff2 / a3afc5e3 / 530d9788), because they were not updated after the 10-13 PR #17 fix. Only the W5-5 row was updated here, as asked.
5. Internal informal proofs (machines/<tm>/proof.md, not public) of W5-3, W5-4, W5-8, #4 and #12b still carry the old wording of the statements Astra corrected. Only the submission/ texts were in scope.
6. Preexisting density warnings keep #4, #4b, #12, #12b and #12b's parent copy short of the zero-warning standard: 11 / 11 / 49 / 21 / 49.
7. Disclosure is mixed inside some bundles (Dennis's call). The rule applied: a text that carries a correction from Astra's audit gets the dual line. In the W5-3, W5-4 and W5-7 bundles every text is dual. W5-3's README got it by a disclosure-only edit, which is the one exception to that rule. In the W4-3, W4-3b, W4-3c, W5-8, W5-8b, W5-8c, #4, #4b, #12 and #12b bundles, the corrected write-ups and READMEs are dual, and the discord drafts and the uncorrected READMEs keep the Claude-only line. In the W5-5 bundle only the .v header is dual. Pick one rule per bundle: all-dual, or dual only where corrected. Then align the drafts. The W4-3 family discord.md is the record of the message posted on 10-13, so it should not be edited.
8. Mailbox. coord/mailbox/to-claude/READ lists 20261014-091339 now, so that item is closed. 20261014-100839 (Astra's hash correction) is answered by 20261014-101245-claude-fix-round-hashes.md and appended to READ. 20261014-100821 (three mechanism studies funded, patch identities acknowledged) is left unread in READ for the orchestrator, because its study and decision items are the orchestrator's.
9. W5-8b and W5-8c .v comments state the map in the reversed direction. This is the same wrong statement Astra corrected in their write-ups. The W5-8b submission .v, lines 347-349, says "Every cell (q, s) of flip tm ... is tmP's cell (phi q, s) with every target state t replaced by phi t". The W5-8c submission .v, lines 399-402, says the same for tm, and so do the source copies. Astra's audit flagged only the write-ups, and there is no header patch for these files, so they were not changed. A comment-only fix would match the write-ups: "tm(q,s) = (w,d,t) -> tmP(phi q,s) = (w,d,phi t)". It would change both shas and need a fresh check_kill each, new hashes in queue.tsv and status.json, and a note to Astra. These files are not upstream yet, so the fix can still go in before submission. Dennis's or the orchestrator's call.
10. The W4-3 family's posted Discord message (10-13) says "every long gap 9x longer". The READMEs, write-ups and PR body are corrected. A correction draft is in machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/submission/family/discord_correction.txt. Posting it is Dennis's call. - 2026-10-14 orchestrator: W4-3 family local write-ups/READMEs: .v line counts 2,583->2,584 and 2,621->2,622 (after the 10-13 comment-only header fix); copies kept byte-identical; pr_body.md (posted) left as the record.