DONE: HPE axiom-probe coverage audit and proposed repair (PR1608)

[bbMisk]

DONE — PR1608, head 26e984849677a26109f2d05393d6de6cd9e50f5f. Claim completed and released.

The standalone HPE driver can print PASS after losing its intended axiom coverage: an import-only probe file reports zero results, and legal indentation makes all 42 queries invisible to its column-zero inventory extraction. The current pinned file already has the correct 42 queries; no invalid accepted HPE theorem or false selected bound is established.

The source-bound package supplies a proposed repair requiring the exact 42-name inventory before building and exactly one allowed-axiom report per name afterward. Frozen source and evidence files are unchanged. The general command/report coverage principle is credited prior work in WeberChen8128's PR893; the distinct result is this HPE reproduction and repair.

Validation: 100 original/repaired driver cases with substituted subprocess results, six adversarial groups rejecting four weakened repairs plus source/receipt/transcript corruption, and all 20 repository research-workflow tests. Optimized isolated CPython3.14 replay matches the receipt. A separate actual Lean4.21 run reproduces the three-probe syntax fixture, including the deliberately forbidden dependency. No HPE/Mathlib rebuild or full selected-construction replay was run. Hosted CI was queued when the published PR was checked; no merge or hosted-CI success is claimed.

Reproduce on Python3.12:

python3.12 -I -B scripts/research_package.py --package research/hpe-axiom-inventory-audit

Research started from main ebedc0895eb4c06725af020bc1af165722b0a3ce and was submitted on refreshed main 81e81af67714bdc8d1693b0bf5c29468b92f62ff. All 21 consumed inputs remained byte-identical. The final focused overlap refresh covered 733 open PRs and 244 Discussion records with complete pagination; it does not search every diff. Scope changed from formal-interface-lemma to this coverage prerequisite and is recorded in TASK.json. The open next question is full-build adoption of the proposed patch in a separately pinned successor.

Credit Jeremy Kothe/jeremykothe2 (PR593), DreamingOfClouds (PR599 and LemmaA/G), commdata2338 (complementary HPE semantic audit PR1415), WeberChen8128 (PR893), and the retained source notices. Prepared for Hanson Sun (@bbMisk) with substantial OpenAI Codex assistance; no subagents or independent human review. Apache-2.0. Emulate was unavailable; prose was checked directly against source and executed evidence under the donor's disclosure instruction.

[bbMisk]

DONE — actual Lean/Mathlib follow-up completed. Full source-pinned finding and real canonical transcript.

Base main ee055dc; PR1608 26e9848. All 53 tested input files remain unchanged at refreshed main 0a20199.

The initial local HPE build passed on Lean4.21.0/Mathlib308445d with the Mathlib cache. The exact repair preserves all 42 real axiom reports and handles legal indentation. Empty, one-missing, duplicate and unexpected query inventories all reject before building. Ten actual driver cases were recorded; successful follow-up cases reuse the unchanged compiled local libraries. No subprocess output was substituted. The full finding includes the source/patch hashes, commands, table and raw repaired transcript.

This closes the stated full-build compatibility question for this environment. It does not run --instances, rebuild the selected supplier, add a theorem or change kappa. Adoption/source-pin updates, hosted CI and inherited physical/all-size/analytic obligations remain separate. No duplicate PR was created; this claim is released. Credit Jeremy Kothe PR593, DreamingOfClouds PR599/LemmaA/G, PR1608 and WeberChen8128 PR893. Prepared for Hanson Sun with substantial OpenAI Codex assistance; no independent human peer review.