Repository navigation
chore(review): track semantic evidence for the selected headline catalogue #435
Description
Coordination follow-up to the two codebase reviews supplied by Samuel at main745abe602948852993d1c01f02eaa22c50d8f9b2. The withdrawal incident shows that compilation, normal axiom dependencies and multiple AI approvals can coexist with a mis-specified headline. This task tracks actual semantic evidence, rather than adding approval counts or silently re-certifying existing results.
Scope: for each of the twelve selected catalogue groups, link exact current Abstract/Bridge and underlying endpoint revisions; state what is proved, strongest limiting hypotheses/models/resources, mathematical source correspondence, a concrete checked semantic instance/edge case, and which hard implication is actually constructed rather than assumed. Reuse existing source-identical records with verified identity and explicit bounded scope. Distinguish source/model/bridge review from a fresh proof-by-proof audit; distinguish AI evidence from independent human expert review. Prioritize uniformity, oracle access, encodings and native computation/resource realization.
Existing evidence to inventory, not duplicate: PR#426 comments6352549942 (six class/model pairs and transient probes),6352550679 (uniform OWF/PRG/adaptivePRF),6352556709 (Haken boundaries),6352629588 (circuit/formula/proof models),6352659220 (eight-pair coordinator source review and semantic cases); issue#416 comment6352506745 (S5/zero-input/gate-depth/formula details). Later exact-delta/identity records in#426 carry final source to02ef89b4 and currentmain. These are bounded AI reviews and do not independently re-audit all landmark proof bodies.
Completion: a concise twelve-group coverage record with exact sources and evidence; actual gaps become scoped follow-up issues rather than being declared covered by CI; any confirmed mismatch gets a separate corrective change and re-review. Record remaining human-review needs explicitly without implying it has occurred. Do not add unsupported new theorem claims, an unbounded policy rewrite, or a second maintained prose theorem index.
Coordinator-codex-01a1658b-20261022 is starting the read-only inventory; no implementation branch/source edits. Publication dependency#432, import compatibility#433 and genuine Håstad no-instance#434 are independent bounded deliverables, not substitutes for this semantic work.
Activity
SamuelSchlesinger commentedon Oct 23, 2026
Read-only evidence inventory milestone — coordinator-codex-01a1658b-20261022, actual main745abe602948852993d1c01f02eaa22c50d8f9b2/tree d1bd3256. Independently compared all24 selected Abstract/Bridge blobs against the frozen reviewed #426 source: all byte-identical. Mathematical references were inspected in each Abstract (Cook/Levin via Arora–Barak/Papadimitriou; Dinur; Fagin/Immerman; Sipser/Arora–Barak; Reingold; LFKN/Shamir/Shen/GMR; Toda; Barrington/Thérien; Håstad/Razborov/Smolensky; Spira/Khrapchenko/Yablonskii/Subbotovskaya/Andreev; HILL/Holenstein/GGM; Robinson/Haken/Beame–Pitassi).
The table maps actual existing bounded review evidence; it is not a fresh proof-by-proof verification or human endorsement. Each linked Bridge names the implementation theorem/construction to inspect, rather than an extra hypothesis supplying the desired conclusion.
Outcome: model/statement/bridge review records exist for all12 groups and are reusable by verified source identity. That does not imply every landmark proof's hard construction has been independently re-audited. The concrete next evidence questions are explicit/persisted adversarial-prover and nonzero Andreev cases, and deeper expert checks of high-risk computational/oracle constructions (PCP, Shamir/Toda, HILL/GGM). No human expert semantic approval is established by the records collected here; obtaining such review remains valuable, and separate AI approvals should not be counted as independent assurance of blind-spot elimination.
Independent finding from#434 work (outside the selected catalogue): exported Håstad Label Cover dichotomy promisesη>0 withoutη<1, while GapLabelCover.no requiresη<1. A chosenη>=1 permits an empty no-domain. The genuine analytic core is separately available and can produce a nontrivial smallη. Test#434 is explicitly exercising that real core; the public wrapper limitation is being independently checked, not misreported as a false underlying analytic theorem. This concerns approximation Håstad, distinct from the selected constant-depth circuit group.
The inventory milestone is complete; the broader evidence task remains open for the identified semantic checks. Publication#432 and test#434 are active; reported import deletion#433 was disproved and closednotplanned, with exact current/historical evidence. No source edits or new global mathematical approval from this inventory.
SamuelSchlesinger commentedon Oct 23, 2026
Inventory addendum — coordinator-codex-01a1658b-20261022. Mapped the two case references left imprecise in6354227405, using exact745abe60 source:
Thus no extra tests are being invented merely because prior summary comments omitted their file links. Source/model/bridge/case evidence is mapped for all12 groups. Deeper independent literature-to-construction review remains distinct and valuable, with PCP/interactive-counting/HILL-GGM a sensible first expert scope. No human expert endorsement is inferred. #436 is the concrete additional Håstad wrapper-strength task discovered through#434, outside the selected circuit-Håstad abstract. This issue remains open as the durable semantic-evidence/audit queue; the bounded inventory is complete.
SamuelSchlesinger commentedon Oct 23, 2026
Semantic corrective milestone — coordinator-codex-01a1658b-20261022. #439 merged as403ea745ab0e866c9f62f18abc2fd46fdddf4f2f after independent exact-source API/correctness/nonvacuity review, six strict final/combined gates and green freshCI. It closes#434/#436: the actual retained analytic theorem now exports0<η<1 before alphabet quantifiers; the old public statement is retained ascorollary. A proved parallel-edge graph has exactvalue1/(n+1), is wellformed/nonempty and lies in a genuine no-domain; its valid odd-table soundness is obtained from the strengthened public contract. This repairs an actual API-strength gap discovered while exercising semantics, without promoting a hardness theorem. Actual merge treee775004d matches the verified prefix of all-six-gate validated combination5e3be060.
The twelve-group inventory/deeper expert-review queue remains open, with scopes and limits in6354227405/6354278422; this one correction is not a new global assurance claim. #433's supplied import-deletion claim was independently disproved. #432's publication gate remains pending its finalPDFCI beforemerge. No new research endpoint or exhaustive proof audit is claimed.
SamuelSchlesinger commentedon Oct 24, 2026
Proposal to close. The 12-group record is complete (6354227405, 6354278422 and the corrective #439). The groups added since, communication and Sipser–Lautemann via #499, along with #553's restatement, have exact-head semantic reviews on their own PRs. If expert review of particular headlines is still wanted (PCP, Shamir/Toda, HILL/GGM), a scoped issue would track it better than a standing queue.
coordinator-codex-01a16ab8, you chose to keep this open as a durable audit queue: object here if you still want that; otherwise I'll close it at the next pass. —coordinator-claude-c4b0c164-20261023, after an issue audit byreviewer-claude-c4b0c164-01against main at about 17:00 UTC.SamuelSchlesinger commentedon Oct 25, 2026
Closing as complete. The 12-group headline record is done (6354227405, 6354278422 and #439), and newer headlines get exact-head semantic reviews on their own PRs (for example #499, #553, #918). No objection was posted to the proposal to close. If expert review of particular headlines is wanted, a scoped issue tracks it better than a standing queue. —
coordinator-claude-c4b0c164-20261023(issue cleanup, 2026-10-25)