diff --git a/.github/workflows/erdos625-sharp-deficit-product.yml b/.github/workflows/erdos625-sharp-deficit-product.yml index d04aead0..01b3689a 100644 --- a/.github/workflows/erdos625-sharp-deficit-product.yml +++ b/.github/workflows/erdos625-sharp-deficit-product.yml @@ -7,7 +7,12 @@ on: - "625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean" - "625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md" - "625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex" + - "625/arxiv/main.tex" + - "625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md" + - "625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json" - "625/experiments/section8_sharp_deficit_product.py" + - "625/experiments/extract_line_by_line_audit_map.py" + - "625/experiments/check_line_by_line_audit.py" - ".github/workflows/erdos625-sharp-deficit-product.yml" workflow_dispatch: @@ -102,3 +107,49 @@ jobs: name: erdos625-sharp-deficit-product-log path: /tmp/erdos625-sharp-deficit-product.log if-no-files-found: ignore + + line-by-line-theorem-audit: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Compile audit tools + run: | + python -m py_compile 625/experiments/extract_line_by_line_audit_map.py + python -m py_compile 625/experiments/check_line_by_line_audit.py + - name: Run audit consistency checker + id: audit-check + continue-on-error: true + shell: bash + run: | + set +e + python 625/experiments/check_line_by_line_audit.py \ + > /tmp/erdos625-line-audit-check.log 2>&1 + status=$? + cat /tmp/erdos625-line-audit-check.log + exit $status + - name: Upload audit checker log + if: always() + uses: actions/upload-artifact@v4 + with: + name: erdos625-line-audit-check-log + path: /tmp/erdos625-line-audit-check.log + if-no-files-found: error + - name: Run audit checker with optimization + if: steps.audit-check.outcome == 'success' + run: python -O 625/experiments/check_line_by_line_audit.py + - name: Generate exact source-map artifact + if: steps.audit-check.outcome == 'success' + run: | + python 625/experiments/extract_line_by_line_audit_map.py \ + 625/arxiv/main.tex \ + --output /tmp/ERDOS625_GENERATED_SOURCE_MAP.md + - name: Upload generated source map + if: steps.audit-check.outcome == 'success' + uses: actions/upload-artifact@v4 + with: + name: erdos625-generated-source-map + path: /tmp/ERDOS625_GENERATED_SOURCE_MAP.md + if-no-files-found: error + - name: Fail if audit checker failed + if: steps.audit-check.outcome == 'failure' + run: exit 1 diff --git a/625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md b/625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md new file mode 100644 index 00000000..54d3abd8 --- /dev/null +++ b/625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md @@ -0,0 +1,653 @@ +# Erdős 625: literal line-by-line and theorem-by-theorem audit + +**Audit date:** 27 July 2026 +**Canonical source audited:** `625/arxiv/main.tex` +**Source blob:** `c4d090b73cd5efcdb98cc30f79bb5f53c6c9bc97` +**Audit branch:** `agent/625-line-by-line-theorem-audit-v2` +**Parent mathematics branch:** PR #49 + +## 1. Scope and standard of review + +This audit treats the canonical TeX as a mathematical dependency graph, not as +one continuous essay. Every boxed theorem, lemma, and proposition is assigned +an exact source range, a proof range, a status, its first downstream use, and +an explicit repair when one is needed. Important unboxed claims are audited in +the same way. + +The statuses are: + +- **GREEN:** correct as written and sufficient for its first downstream use; +- **GREEN-REWRITE:** mathematically sound, or supported by a shorter checked + replacement, but the theorem contract or exposition should be rewritten; +- **AMBER:** conditionally correct, with one named missing hypothesis, + uniformity statement, or finite bridge; +- **RED:** not established by the canonical text as written, or downstream of + an unresolved load-bearing result; +- **TYPO/EDITORIAL:** a source defect that does not itself invalidate the + mathematics; +- **SUPERSEDED:** a longer route that should be removed from Version 2 in favor + of a shorter checked argument. + +A line range marked GREEN is not a claim that every displayed asymptotic has a +complete Lean formalization. It means that no mathematical gap was found in +that source argument and that the hypotheses stated or proved there suffice +for the first place where the result is used. + +## 2. Executive verdict + +There is one submission-blocking chain: + +```text +Lemma 8.3 + -> Proposition 9.2 + -> Theorem 1. +``` + +No second unrelated fatal gap was found. Sections 2--7 and Lemmas 10.1--10.2 +are structurally coherent. Lemmas 8.1--8.2 are also coherent and have cleaner +checked replacements. Section 9 is no longer an independent bottleneck because +the direct matching-restriction/q-only route controls the literal attained +attachment sum once the Section VIII bare-skeleton estimate is supplied. + +The blocker is finite and precise: + +> The canonical text does not prove that the entire attained physical +> high-skeleton family is reindexed without multiplicity by a block-level +> matching support, one admissible deficit per selected cell, and the associated +> local partial physical-matching fibres, with the exact aggregate weight. + +The local ratio and global falling-factorial estimate used after that +reindexing are correct. The missing item is the exact global fibre theorem. + +### Boxed-statement count + +| Status | Boxed statements | +|---|---:| +| GREEN | 5 | +| GREEN-REWRITE | 5 | +| SUPERSEDED | 1 | +| RED | 3 | + +The three RED boxed statements are Theorem 1, Lemma 8.3, and Proposition 9.2. +Theorem 1 and Proposition 9.2 are RED only through their dependence on Lemma +8.3; their final logical deductions are valid. + +## 3. Complete source-range map + +| Source lines | Content | Status | Audit conclusion | +|---:|---|---|---| +| 1--72 | Preamble and metadata | TYPO/EDITORIAL | The date and publication metadata are stale relative to the current audit. Mathematical content unaffected. | +| 73--98 | Abstract | RED | It says “We prove” before the load-bearing Section VIII theorem is closed. Use the audit-safe abstract until closure. | +| 99--225 | Introduction, Theorem 1, background, roadmap | MIXED | Theorem 1 is RED; the background and three-layer roadmap are useful but describe the old Sections VIII--IX rather than the shorter replacement route. | +| 227--292 | Notation and inequalities (1.1)--(1.5) | GREEN | Stirling, McDiarmid, Paley--Zygmund, the binomial tail, and Markov are used in valid ranges. | +| 293--447 | Section 2 and Lemma 2.1 | GREEN | Phase expansion, adjacent-size ratios, and the independence-number cap are uniform in the full phase. | +| 448--741 | Section 3 and Lemma 3.1 | GREEN-REWRITE | Correct continuous-root architecture, but one lemma currently contains several logically independent analytic theorems. | +| 742--797 | Section 4 | GREEN | The chromatic lower location is genuinely unrestricted after the probabilistic size cap. | +| 798--1307 | Section 5 and Lemma 5.1 | GREEN-REWRITE | Root displacement and integer rounding are coherent. The entropy certificate and final constant can be strengthened substantially. | +| 1308--1524 | Section 6 and Lemmas 6.1--6.2 | GREEN | Exact sign sum and prescribed-cell configuration bound are correct and reusable. | +| 1525--1936 | Section 7 and Lemma 7.1 | GREEN-REWRITE | Exact recurrences and three-range proof are coherent. Fix the TeX exponent typo and replace decimal rate checks by the exact certificate. | +| 1937--2149 | Section 8 definitions and Lemma 8.1 | GREEN-REWRITE | Canonical high support and endpoint transport are sound; use the square-free checked presentation. | +| 2150--2230 | Lemma 8.2 | GREEN-REWRITE | The Cauchy proof works, but termwise square-free AM--GM is shorter and avoids a polynomial loss. | +| 2231--2491 | Lemma 8.3 | RED | The exact attained-demand/physical-fibre reindexing and aggregate weight identity are not established. Replace the entire near/middle route. | +| 2492--2548 | Exact conditional decomposition (9.1)--(9.2) | GREEN-REWRITE | Correct target; synchronize it with the literal attained-attachment formalization. | +| 2549--2828 | Lemma 9.1 | SUPERSEDED | The old cycle/walk proof is unnecessary. Use matching restriction and the q-only two-regime theorem. | +| 2829--2866 | Proposition 9.2 | RED | Its final multiplication is correct, but it depends on RED Lemma 8.3. | +| 2867--2964 | Lemma 10.1 | GREEN | The simultaneous leftover coloring argument is valid. | +| 2965--3047 | Lemma 10.2 | GREEN | The seed-to-typical bounded-differences amplifier is valid and uniform in deterministic parameters. | +| 3048--3077 | Application of amplification | AMBER | Analytic scales are correct conditional on Proposition 9.2. | +| 3078--3111 | Completion of proof | RED | Union-bound intersection and subtraction are correct, but depend on Proposition 9.2. | +| 3112--3161 | Reproducibility, AI, funding, references | EDITORIAL | The statement that the Lean formalization is partial is accurate. Synchronize all theorem-status language before publication. | + +## 4. Front matter and notation: lines 1--292 + +### Lines 1--72: metadata + +- Lines 64--71 define the title, affiliation, date, MSC, and keywords. +- No mathematical issue arises here. +- The canonical date predates the present audit and should not be treated as a + publication-status timestamp. +- The current audit-safe policy is to keep theorem claims conditional until the + blocking chain closes. + +### Lines 73--98: abstract — **RED** + +- Lines 77--85 define the two invariants and state the full theorem. +- Line 80 says “We prove”. That sentence is not currently justified because + Proposition 9.2 is not established on the integrated source branch. +- Lines 88--98 give a faithful high-level description of the method, but the + configuration-model/cycle wording reflects the old Section IX route. + +**Required repair.** Use an audit-safe abstract saying that the manuscript +contains a candidate proof whose only unresolved verification seam is the exact +Section VIII physical-fibre reindexing. After closure, replace the method +sentence by the shorter all-deficit and matching-restriction architecture. + +### Lines 99--225: introduction and Theorem 1 + +- Lines 106--112 define the model and invariants correctly. +- Lines 114--119 state the historical question and introduce the result. +- Lines 121--130 state Theorem 1. The numerical constant is positive and would + follow from the current first-moment calculation if Proposition 9.2 were + established. The theorem is nevertheless **RED at present**. +- Lines 132--137 correctly emphasize the full-sequence phase issue. +- Lines 139--186 give relevant historical context. The bibliography should be + synchronized with the later literature audit, including the foundational + cochromatic and generalized-coloring references. +- Lines 188--225 give a useful dependency roadmap, but Sections VIII--IX should + be described using the Version 2 route rather than the old near/middle and + cycle-walk machinery. + +### Lines 227--292: elementary inputs — **GREEN** + +- Equation (1.1) is the expected number of \(s\)-vertex independent sets. +- Stirling (1.2) is invoked only with the stated zero-safe \(O(\log(m+1))\) + variant when coordinates may vanish. +- McDiarmid (1.3) is later used with \(n-1\) independent vertex-exposure blocks + and a one-Lipschitz variable. +- Paley--Zygmund (1.4) is used with a finite nonnegative witness count. +- The binomial bound (1.5) follows from exponential Markov; the displayed + numerical exponential is conservative. +- Markov is used in the standard first-moment form. + +No repair is needed. + +## 5. Lemma 2.1: lines 295--322, proof lines 324--437 — **GREEN** + +### Contract + +The lemma must supply: + +1. a phase-uniform expansion for \(\log\mu_\alpha\); +2. \(\mu_{\alpha+2}=o(1)\), to cap all independent sets at size + \(\alpha+1\) with high probability; +3. a uniform polynomial lower bound for \(\mu_{\alpha-2}\), used in the empty + corner of the partial-diagonal sum. + +### Statement audit + +- Lines 297--307 state the expansion with a bounded continuous \(K\). +- Lines 309--314 derive the upper adjacent-size estimate. +- Lines 315--322 state the lower estimate at \(a=\alpha-2\). +- The extension to \(\delta=1\) is harmless: the displayed formula for \(K\) + extends continuously to the closed interval even though the actual phase has + \(\delta<1\). + +### Proof audit + +- **Lines 324--343:** the representation + \(\alpha=2S/\log2+b\), the falling-factorial expansion, and the use of + Stirling are valid because \(\alpha=O(\log n)\) and + \(\alpha^2/n=o(1)\). +- **Lines 344--384:** the Taylor expansion of \(\log\alpha\), multiplication by + \(\alpha\), and the half-log Stirling correction give (2.2). All error terms + are uniform for \(b\in(0,1]\). +- **Lines 385--405:** the adjacent-size ratios are exact. Their uniform + \(\Theta(\log n/n)\) and \(\Theta(n/\log n)\) forms follow from the phase + formula for \(\alpha\). +- **Lines 406--437:** (2.3) and (2.4) follow with the stated exponents; Markov + then gives (2.9). + +### Downstream sufficiency + +- Equation (2.9) is strong enough for the unrestricted refinement argument in + Section 4. +- The lower bound (2.4), together with the finite number of adjacent shifts, + is strong enough for the empty-corner estimate in Section 7. + +**Verdict:** no mathematical repair required. + +## 6. Lemma 3.1: lines 495--561, proof lines 563--740 — **GREEN-REWRITE** + +### Contract + +This lemma simultaneously claims: + +- existence and uniqueness of the two continuous roots; +- their common phase corridor; +- a uniform derivative of order \((\log n)^2\); +- exact support comparison at fixed mean; +- compact-uniform convergence of finite entropy values; +- bounded tilts, positive variance, and uniform optimizer convergence. + +The content is coherent, but this is too much for one lemma. + +### Statement audit + +- The target \(T_0=1+2/\log2-\delta\) remains strictly inside the convex hull + of \(S_4=\{2,3,4,5\}\) and of the truncated \(S_+\) support. +- The root corridor and derivative have the correct scales. +- Equation (3.8) is an exact fixed-mean cancellation of the affine score. +- \(K_*\) is a valid compact target interval contained in \((2,5)\). +- The finite-\(n\) optimizer on \(S_4\) has all four coordinates bounded below + because the limiting Gibbs weights are continuous and strictly positive on a + compact tilt interval. + +### Proof audit + +- **Lines 563--598:** dividing by \(k\) and decomposing + \(-\log d_{\alpha-i}=A_n+B_ni+h_n(i)\) are exact. The separate \(i=-1\) + formula is required and is supplied. +- **Lines 599--645:** Gaussian domination controls the finite \(S_+\) cutoff, + the partition sums, first moments, and variances uniformly. The strict target + inequalities at \(\pm\Lambda\) and the variance floor imply uniformly + Lipschitz inverse mean maps. This justifies compact-uniform convergence and + (3.8)--(3.9b). +- **Lines 646--700:** the scalar exponent at \(s_0\) is \(O(\log\log n)\). + The cancellations in (3.15a)--(3.16) have the correct order. +- **Lines 701--740:** differentiating through the finite optimum is justified + by the unique interior Gibbs optimizer. The derivative is + \(-\log n+O(\log\log n)\) in the \(s\)-coordinate, yielding strict + monotonicity, a unique corridor zero, and the stated \(k\)-derivative. + +### Hidden conditions made explicit + +1. For \(S_+\), every finite-\(n\) sum is truncated at \(i=\alpha-1\). +2. The target interval stays in the relative interior of both finite supports. +3. The variance floor is applied only on the selected compact tilt interval. +4. The envelope derivative is for the unique interior optimizer. + +### Rewrite + +Split the current lemma into: + +1. finite Gibbs dual attainment and exact support comparison; +2. compact-uniform partition/moment/tilt convergence; +3. root corridor and uniqueness; +4. derivative at the root corridor. + +**Verdict:** mathematically sound; rewrite for auditability. + +## 7. Section 4: lines 743--797 — **GREEN** + +- Lines 747--761 define the unrestricted continuous root, the integer lower + location, and the exact unordered-profile expectation. +- Lines 764--780 sum all bounded profiles. There are + \(\exp(O((\log n)^2))\) such profiles, and zero profile coordinates are + handled by the zero-safe Stirling bound. +- Lines 782--795 use the derivative from Lemma 3.1 to move + \(\lceil\log n\rceil\) to the left of the root, producing a negative exponent + of order \((\log n)^3\). +- On the event \(\alpha(G_n)\le\alpha+1\), any coloring with at most + \(k_\chi^-\) parts can be split into exactly \(k_\chi^-\) nonempty independent + parts. Since \(k_\chi^-\log(1000/639). +\] + +The stronger certificate should replace the current long tail ledger. + +## 9. Root displacement and midpoint profile: lines 1123--1307 — **GREEN-REWRITE** + +- **Lines 1123--1173:** the \(2^k\) signed gain is exact because all class sizes + are at least two for large \(n\), so the independent and complete declarations + are disjoint. +- **Lines 1174--1212:** the mean-value theorem, root corridor, and derivative + give + \[ + r_+-r_4^{\mathrm{co}} + =\left(\frac{(\log2)^2}{4} + (\log2-D_4(\delta))+o(1)\right) + \frac n{(\log n)^3}. + \] +- **Lines 1213--1248:** the midpoint integer and the two-coordinate correction + enforce both conservation laws. The correction has bounded size and + positivity follows from \(k_i=\Theta(n/\log n)\). +- **Lines 1249--1260:** the displacement is tangent to both constraints. The + Hessian calculation gives an \(O(1/k)\) loss, stronger than needed. +- **Lines 1261--1307:** the exact signed first moment is exponentially large in + \(k\), and a positive signed witness gives a genuine cocoloring. + +The text loses more constant than required. Midpoint placement retains the +coefficient \((\log2)^2/8\), and integer rounding and amplification are lower +order. After Section VIII closure, the natural theorem is + +\[ + \chi(G_n)-\zeta(G_n) + \ge + \left[ + \frac{(\log2)^2}{8}(\log2-D_4(\delta_n))-o(1) + \right] + \frac n{(\log n)^3}. +\] + +The stronger certified fixed coefficient is + +\[ + \frac{(\log2)^2}{8}\log(1000/639) + =0.026896409808379\ldots. +\] + +## 10. Lemma 6.1: lines 1354--1383, proof lines 1385--1428 — **GREEN** + +- **Lines 1385--1394:** label slots. This deterministic labeling factor cancels + in the normalized second moment. +- **Lines 1395--1405:** signs must agree across every overlap cell of size at + least two, so they are constant on components of \(H\). Isolated row and + column slots retain independent signs. +- **Lines 1406--1418:** \(W\) internal edge bits are prescribed twice. Dividing + by the two marginal signed probabilities gives the first exact formula. +- **Lines 1419--1428:** split one unit from each support-edge exponent and use + \(|E|-|V|+c=\beta\) to obtain the local/topological factorization. + +No gap was found. Equation (6.7), lines 1429--1443, is the standard binary +cycle-space cardinality identity and is also GREEN. + +## 11. Lemma 6.2: lines 1445--1482, proof lines 1484--1523 — **GREEN** + +- **Lines 1445--1482:** feasibility conditions and both probability bounds are + stated with the correct zero cases. +- **Lines 1484--1501:** selecting disjoint row and column stubs and then local + bijections produces exactly + \(\prod_a(d_a)_{D_a}\prod_b(d'_b)_{D'_b}/\prod x_{ab}!\) + witnesses. +- **Lines 1502--1505:** a fixed witness has probability \(1/(m_0)_x\). +- **Lines 1506--1523:** the binomial and factorial inequalities yield + \((m_0)_x\ge(m_0/e)^x\), after which falling factorials are bounded by powers. + +The crucial feature is preserved: the exact result keeps one global +\((m_0)_x\) denominator before taking the cellwise product majorant. + +## 12. Lemma 7.1: lines 1651--1659, proof lines 1667--1935 — **GREEN-REWRITE** + +### Exact identities before the lemma + +- The marked partial-diagonal definition is deliberately an overcount by + nonnegative marked terms; no disjointness is claimed. +- **Source defect:** equation (7.2) writes `2^\ell_\bullet`. It must be + `2^{\ell_\bullet}`. +- Equations (7.3)--(7.6) follow by exact factorial cancellation and one-coordinate + ratios. + +### Empty corner: lines 1667--1704 + +The lower bound on \(\mu_{u_i}(n)\) gives +\(\Xi_{\mathrm{empty}}=o(1)\). Iterating the exact recurrence while selected +mass is at most \(\eta n\) produces a product of exponential-series terms whose +total is \(1+o(1)\). + +### Central range: lines 1705--1906 + +- Lines 1705--1723 introduce normalized selected and residual profiles and the + exact residual vertex fraction. +- Lines 1724--1785 apply zero-safe Stirling and isolate the four coordinate + costs \(E_i\). +- Lines 1786--1847 use the signed first-moment margin to control the affine + average and derive the rate function. +- Lines 1848--1878 prove uniform negativity by two convex endpoint checks. The + decimal inequalities should be replaced by the exact rational certificate + from the later audit stack. +- Lines 1879--1906 show that the negative leading term dominates entropy and + logarithmic errors uniformly away from both corners. + +### Full corner: lines 1907--1935 + +The adjacent-size estimates and the factor \(32^{-u_i}=n^{-10+o(1)}\) make the +reverse recurrence decreasing. Division by the exponentially large complete +signed first moment makes the full corner negligible. + +## 13. Lemma 8.1: lines 2053--2079, proof lines 2081--2146 — **GREEN-REWRITE** + +The global falling-factorial comparison follows from concavity of +\(f(x)=\log(n)_x\) and the exact mass identity (8.11). The local unequal-size +factor follows from (8.13), and the phase relation gives the stated \(\eta_n\). + +The square-root-free cross-multiplied theorem from the later formal stack is +safer: it handles positivity before cancellation and makes endpoint cases +total. Use that theorem as the primary statement. + +## 14. Lemma 8.2: lines 2151--2169, proof lines 2171--2228 — **GREEN-REWRITE** + +Cauchy's inequality and the two nonnegative domain enlargements are valid. The +multinomial theorem gives the one-sided row and column sums, and Lemma 7.1 +closes the diagonal sum. + +The termwise square-free AM--GM route is shorter and yields + +\[ + \sum_L W(L) + \le (1+C\eta_n)^{k_{\mathrm{co}}}\sum_rD(r) +\] + +directly, without \((\sum\sqrt D)^2\). + +## 15. Lemma 8.3: lines 2233--2243, proof lines 2245--2490 — **RED** + +This is the only independent submission blocker. + +### Proof introduction: lines 2245--2263 + +The near/middle charging narrative announces an objectwise completion picture. +That picture is not literal: a partial physical matching generally has many +full completions and may leave stubs that participate in residual cells. + +### Step I: lines 2264--2284 + +Writing \(j=m-e\) is unique, and the high/middle inequalities are correct. +Replacing selected multiplicities by full endpoint multiplicities gives a +valid block-level reference table. What is missing is a weight-preserving +finite theorem connecting the actual physical family to that reference table +and deficit data. + +### Step II: lines 2285--2369 + +- Equation (8.21) is the correct aggregate local ratio after summing the local + partial-stub-matching fibre. +- Equation (8.22) is the correct single global denominator ratio. +- The one-cell near series (8.25) is valid. +- **Blocking transition:** equations (8.25a)--(8.26) and the sentence + “distinguishing and then forgetting identical typed cells is exactly the + multinomial expansion” do not prove the required global physical-fibre + decomposition. + +### Steps III--IV: lines 2370--2469 + +The joint threshold estimate is applied before constraints are relaxed, so the +upper-bound direction is preserved. However, finite sums use the nonliteral +range \(3a/4+O(1)\), and Step IV pays residual local and cycle factors despite +the section contract saying those factors are deferred. + +### Assembly: lines 2470--2490 + +The assembly would be valid if the preceding exact fibre inequality were +proved. It does not repair that missing theorem. + +### Required replacement + +Prove an exact decomposition by block support, admissible deficits, and local +partial physical matching fibres. Then use + +\[ + \frac{w(P,m-h)}{w_{\mathrm{full}}(P)} + \le \prod_e n^{h_e}R_{m_e,d_e}(h_e) +\] + +with the global denominator charged once. The checked sharper arithmetic gives + +\[ + h\left\lfloor\frac{3m-1}{4}\right\rfloor + \le hm-\frac{h(h+1)}2 +\] + +for \(2h Lemma 3.1 + -> Section 4 chromatic lower location + -> Lemma 5.1 and four-size root displacement + -> exact midpoint profile and signed first moment + +Lemma 6.1 + Lemma 6.2 + -> Lemma 7.1 partial diagonals + -> endpoint reference normalization and transport + -> exact attained-demand support/deficit/partial-fibre reindexing [OPEN] + -> cellwise all-deficit product + -> bare-skeleton estimate [OPEN] + +matching restriction + q-only two-regime attachment + -> normalized second moment [OPEN only through bare skeleton] + -> Paley--Zygmund seed + +Lemma 10.1 + Lemma 10.2 + -> high-probability cochromatic upper location + +chromatic lower location + cochromatic upper location + -> phase-resolved gap theorem. +``` + +## 24. Acceptance gates before changing theorem status + +The canonical abstract and Theorem 1 may be promoted from RED only after all of +the following are green on one integrated commit: + +1. the actual midpoint profile is proved to satisfy the four-endpoint cover; +2. attained canonical high demands inject into support/deficit data; +3. the partial physical matching fibre has the exact aggregate cardinality; +4. `profileHighSkeletonWeight` is identified pointwise with that aggregate + weight; +5. the one global falling-factorial comparison is applied after the aggregate + fibre sum; +6. the complete positive-deficit fibre is summed cellwise; +7. full-reference supports are identified with the exact endpoint table weights + \(W(L)\); +8. endpoint transport and Lemma 7.1 produce the bare-skeleton estimate; +9. the q-only literal attachment theorem is composed with that estimate; +10. Proposition 9.2 is built warning-fatally with no placeholders or + project-defined axioms; +11. Lemmas 10.1--10.2 and the final event intersection are replayed against the + resulting deterministic error sequence; +12. the TeX, bibliography, source typo, theorem coefficient, Lean status, and + reproducibility language are synchronized. + +## 25. Final audit verdict + +The candidate proof is not a diffuse collection of unchecked claims. The +mathematics before Section VIII and after Proposition 9.2 is substantially +coherent. The exact signed overlap identity and amplification argument are +particularly clean. + +The current canonical TeX is nevertheless not ready to assert Theorem 1. The +one load-bearing finite reindexing in Lemma 8.3 is not proved by its present +“complete, distinguish, and forget” prose. The repair is sharply specified and +supported by several green finite components, but the final pointwise aggregate +weight identification and global bare-skeleton assembly must still be checked. + +Accordingly: + +- **Theorem 1:** RED, conditional on one explicit chain; +- **Lemmas 2.1, 6.1, 6.2, 10.1, 10.2:** GREEN; +- **Lemmas 3.1, 5.1, 7.1, 8.1, 8.2:** GREEN-REWRITE; +- **Lemma 8.3:** RED and the unique independent blocker; +- **Lemma 9.1:** SUPERSEDED by a shorter checked route; +- **Proposition 9.2:** RED only through Lemma 8.3. diff --git a/625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json b/625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json new file mode 100644 index 00000000..ec421174 --- /dev/null +++ b/625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json @@ -0,0 +1,281 @@ +{ + "audit_date": "2026-07-27", + "repository": "SamPetkov/Erdos", + "source": "625/arxiv/main.tex", + "source_blob_sha": "c4d090b73cd5efcdb98cc30f79bb5f53c6c9bc97", + "status_legend": { + "GREEN": "Correct as written and sufficient for its first downstream use.", + "GREEN-REWRITE": "Mathematically sound or supported by a checked replacement, but the theorem contract or exposition should be rewritten.", + "AMBER": "Conditionally correct or plausible, with an explicit missing uniformity, finite bridge, or theorem hypothesis.", + "RED": "Not established by the canonical text as written, or downstream of an unresolved load-bearing result.", + "TYPO/EDITORIAL": "A source-level defect that does not by itself invalidate the mathematical argument.", + "SUPERSEDED": "A longer route that should be replaced by a shorter checked argument before Version 2 publication." + }, + "single_blocking_chain": [ + "Lemma 8.3", + "Proposition 9.2", + "Theorem 1" + ], + "items": [ + { + "id": "T1", + "kind": "theorem", + "title": "Theorem 1", + "statement_lines": [119, 130], + "proof_lines": [3078, 3111], + "status": "RED", + "blocking": true, + "dependencies": ["C4", "C5", "P9.2", "L10.2"], + "first_downstream_use": "Abstract and claimed full-sequence resolution.", + "issue": "The final probability intersection is valid, but Proposition 9.2 remains downstream of the unresolved exact Section VIII all-deficit reindexing and weight identity.", + "repair": "Keep the theorem conditional or replace the abstract by audit-safe status language until the integrated Section VIII theorem and Proposition 9.2 are green. After closure, promote the phase-resolved /8 coefficient and the stronger uniform entropy certificate." + }, + { + "id": "L2.1", + "kind": "lemma", + "title": "Lemma 2.1 (phase expansion)", + "statement_lines": [295, 322], + "proof_lines": [324, 437], + "status": "GREEN", + "blocking": false, + "dependencies": ["Eq. (1.2)"], + "first_downstream_use": "Independence-number cap (2.9), root phase, and endpoint phase asymptotics.", + "issue": "No mathematical gap found. Uniformity in the phase is correctly preserved; the continuous extension of K to delta=1 should simply be stated as an extension of the displayed polynomial expression.", + "repair": "Minor prose tightening only." + }, + { + "id": "L3.1", + "kind": "lemma", + "title": "Lemma 3.1 (root phase, derivative, and support comparison)", + "statement_lines": [495, 561], + "proof_lines": [563, 740], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["L2.1", "finite entropy duality", "uniform Gaussian tails"], + "first_downstream_use": "Chromatic root location, signed root displacement, and midpoint first-moment margin.", + "issue": "The proof is coherent, but several logically distinct results are bundled into one long lemma: finite dual attainment, compact-uniform convergence, bounded tilts, variance floor, root corridor, derivative, and support difference.", + "repair": "Split into four named lemmas and state the finite cutoff and interior-feasibility conditions before invoking the envelope theorem." + }, + { + "id": "C4", + "kind": "unboxed claim", + "title": "Unrestricted chromatic lower location", + "statement_lines": [743, 797], + "proof_lines": [743, 797], + "status": "GREEN", + "blocking": false, + "dependencies": ["L2.1", "L3.1"], + "first_downstream_use": "Final event intersection.", + "issue": "No hidden profile restriction remains: the independence-number event supplies the size cap and splitting refines a coloring to exactly k_chi^- nonempty parts.", + "repair": "Promote equation (4.5) to a named proposition for navigability." + }, + { + "id": "L5.1", + "kind": "lemma", + "title": "Lemma 5.1 (uniform entropy certificate)", + "statement_lines": [860, 869], + "proof_lines": [871, 1121], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["L3.1", "explicit Gaussian-tail inequalities"], + "first_downstream_use": "Root displacement (5.11) and the signed first-moment margin.", + "issue": "The displayed certificate is valid but nonoptimal and the proof is longer than necessary. Later exact certification yields D_4(delta)log(1000/639).", + "repair": "Replace the current tail ledger by the stronger exact certificate and isolate the tilt bracket, omitted-mass estimate, and entropy conclusion as separate sublemmas." + }, + { + "id": "C5", + "kind": "unboxed claim", + "title": "Four-size root displacement, integer midpoint profile, and signed first moment", + "statement_lines": [1123, 1307], + "proof_lines": [1123, 1307], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["L3.1", "L5.1"], + "first_downstream_use": "Definition of the exact midpoint witness and deterministic gap (5.20).", + "issue": "The root displacement, tangent rounding, and positive signed first-moment margin are coherent. Two conservative halvings weaken the final constant: midpoint placement retains a /8 coefficient, not merely the printed /32 coefficient.", + "repair": "State a phase-resolved proposition with coefficient (log 2)^2/8*(log 2-D_4(delta_n)), followed by the stronger uniform corollary." + }, + { + "id": "L6.1", + "kind": "lemma", + "title": "Lemma 6.1 (exact sign sum)", + "statement_lines": [1354, 1383], + "proof_lines": [1385, 1428], + "status": "GREEN", + "blocking": false, + "dependencies": ["exact overlap law (6.2)"], + "first_downstream_use": "All second-moment overlap estimates.", + "issue": "No gap found. The compatible-sign count, duplicated-edge-bit correction, and cycle-rank factorization are exact.", + "repair": "Add a one-component worked example; no mathematical repair required." + }, + { + "id": "C6.7", + "kind": "unboxed claim", + "title": "Binary cycle-space identity (6.7)", + "statement_lines": [1429, 1443], + "proof_lines": [1429, 1443], + "status": "GREEN", + "blocking": false, + "dependencies": ["elementary F_2 cycle-space dimension"], + "first_downstream_use": "Residual even-subgraph expansion.", + "issue": "No gap found.", + "repair": "Optionally name it as a corollary of Lemma 6.1." + }, + { + "id": "L6.2", + "kind": "lemma", + "title": "Lemma 6.2 (joint prescribed-cell bound)", + "statement_lines": [1445, 1482], + "proof_lines": [1484, 1523], + "status": "GREEN", + "blocking": false, + "dependencies": ["uniform bipartite configuration model"], + "first_downstream_use": "Threshold-demand bounds in Sections VIII and IX.", + "issue": "No gap found. The witness count retains the single global falling factorial before the product majorant is taken, and infeasible cases are explicitly empty.", + "repair": "No mathematical repair required." + }, + { + "id": "L7.1", + "kind": "lemma", + "title": "Lemma 7.1 (all common subprofiles)", + "statement_lines": [1651, 1659], + "proof_lines": [1667, 1935], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["C5", "exact recurrences (7.4) and (7.6)"], + "first_downstream_use": "Endpoint transportation sum in Lemma 8.2.", + "issue": "The three-range architecture is coherent. Equation (7.2) contains the TeX typo 2^\\ell_\\bullet. The central-rate proof relies on decimal endpoint checks that have a stronger exact rational replacement in the later audit stack.", + "repair": "Fix the exponent braces, replace decimal certificates by the exact rate certificate, and state all central-range error terms uniformly in the phase." + }, + { + "id": "L8.1", + "kind": "lemma", + "title": "Lemma 8.1 (geometric-mean transportation comparison)", + "statement_lines": [2053, 2079], + "proof_lines": [2081, 2146], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["L7.1", "exact endpoint normalization"], + "first_downstream_use": "Sum of endpoint tables in Lemma 8.2.", + "issue": "The falling-factorial concavity and local unequal-size algebra are sound. Later Lean work proves a denominator-free square-free form and the exact endpoint reference normalization, which is safer and easier to audit.", + "repair": "State the square-free transport theorem first and derive the displayed geometric-mean inequality as a corollary only if still desired." + }, + { + "id": "L8.2", + "kind": "lemma", + "title": "Lemma 8.2 (sum of all endpoint tables)", + "statement_lines": [2151, 2169], + "proof_lines": [2171, 2228], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["L7.1", "L8.1"], + "first_downstream_use": "Reference measure in Lemma 8.3.", + "issue": "The Cauchy-multinomial proof is a valid nonnegative enlargement, but it introduces a needless (sum sqrt D)^2 step and a polynomial margin-count loss.", + "repair": "Use the checked square-free AM-GM linearization and one-sided multinomial sums, yielding sum_L W(L) <= exp(O(sqrt(n log n))) sum_r D(r) directly." + }, + { + "id": "L8.3", + "kind": "lemma", + "title": "Lemma 8.3 (all nonendpoint high multiplicities)", + "statement_lines": [2233, 2243], + "proof_lines": [2245, 2490], + "status": "RED", + "blocking": true, + "dependencies": ["L8.2", "exact attained-demand physical-fibre reindexing"], + "first_downstream_use": "Proposition 9.2 through the skeleton sum in (9.2).", + "issue": "The local ratio (8.21) and single global denominator comparison (8.22) are correct, but the passage to (8.25a) does not prove the exact aggregate fibre decomposition. A partial physical matching generally has many full completions; the text's 'distinguish and forget' sentence is not the required weight-preserving bijection. The middle-strip sums also use the nonliteral range 3a/4+O(1), and Step IV pays residual local/cycle factors despite the section contract deferring them.", + "repair": "Replace the whole lemma by the exact encoding: attained high demand -> block matching support + admissible deficits + local partial stub-matching fibres. Prove the pointwise aggregate weight identity, use the one global (n-J)_H loss, sum deficits cellwise, and then apply endpoint transport. The checked three-quarter budget gives a direct exponent O(sqrt(n)(log n)^(3/2)); an optional head-tail split gives O((log n)^4)." + }, + { + "id": "C9.2", + "kind": "unboxed claim", + "title": "Exact conditional decomposition (9.2)", + "statement_lines": [2492, 2548], + "proof_lines": [2492, 2548], + "status": "GREEN-REWRITE", + "blocking": false, + "dependencies": ["L6.1", "canonical high-support extraction"], + "first_downstream_use": "Proposition 9.2.", + "issue": "The factorization is the correct target and has a later literal attained-attachment formal counterpart. Its exposition should be synchronized with the aggregate physical-fibre language used to repair Lemma 8.3.", + "repair": "State the normalized moment as the attained canonical attachment sum, then factor a pointwise literal attachment bound." + }, + { + "id": "L9.1", + "kind": "lemma", + "title": "Lemma 9.1 (uniform attachment bound)", + "statement_lines": [2550, 2565], + "proof_lines": [2567, 2827], + "status": "SUPERSEDED", + "blocking": false, + "dependencies": ["L6.2", "cycle-space identity"], + "first_downstream_use": "Proposition 9.2.", + "issue": "No counterexample to the stated upper bound was found, but the cycle-family, walk-kernel, and mixed-cycle proof is unnecessarily long. A checked matching-restriction theorem directly bounds the weighted even family by a subset product, and the q-only two-regime theorem controls the literal attained attachment sum.", + "repair": "Replace equations (9.12)-(9.19) by injective restriction outside the exposed matching and one total-q estimate. Keep the small-residual deterministic branch." + }, + { + "id": "P9.2", + "kind": "proposition", + "title": "Proposition 9.2 (normalized signed second moment)", + "statement_lines": [2832, 2842], + "proof_lines": [2844, 2865], + "status": "RED", + "blocking": true, + "dependencies": ["L8.3", "L9.1", "C9.2"], + "first_downstream_use": "Rare-event seed (10.1).", + "issue": "The final multiplication of a uniform attachment bound by the skeleton sum is correct. The proposition is unproved only because Lemma 8.3 is not established by the canonical text.", + "repair": "Compose the future green Section VIII bare-skeleton theorem with the already checked q-only attained-attachment frontier." + }, + { + "id": "L10.1", + "kind": "lemma", + "title": "Lemma 10.1 (simultaneous leftover coloring)", + "statement_lines": [2903, 2912], + "proof_lines": [2914, 2963], + "status": "GREEN", + "blocking": false, + "dependencies": ["binomial tail (1.5)"], + "first_downstream_use": "Leftover coloring in Lemma 10.2.", + "issue": "No gap found. The density event is simultaneous, averaging propagates it to larger sets, and the greedy complement-neighborhood process constructs independent sets of logarithmic size.", + "repair": "Minor constant simplification only." + }, + { + "id": "L10.2", + "kind": "lemma", + "title": "Lemma 10.2 (amplification from a seed)", + "statement_lines": [2968, 2989], + "proof_lines": [2991, 3046], + "status": "GREEN", + "blocking": false, + "dependencies": ["L10.1", "bounded differences (1.3)"], + "first_downstream_use": "High-probability cocoloring upper location (10.13).", + "issue": "No gap found. The induced cocolorable-capacity variable is one-Lipschitz under vertex-block exposure, and the simultaneous leftover event supplies an epsilon_n independent of the deterministic parameters.", + "repair": "Promote the tunable tail family (10.5) as a named corollary in Version 2." + }, + { + "id": "C10", + "kind": "unboxed claim", + "title": "Application of the amplifier to the midpoint seed", + "statement_lines": [3047, 3077], + "proof_lines": [3047, 3077], + "status": "AMBER", + "blocking": false, + "dependencies": ["P9.2", "L10.2"], + "first_downstream_use": "Final event intersection.", + "issue": "All scale calculations are correct conditional on Proposition 9.2. The claim must retain that dependency explicitly.", + "repair": "No analytic repair beyond closing Proposition 9.2." + }, + { + "id": "C11", + "kind": "unboxed final proof", + "title": "Completion of the proof", + "statement_lines": [3078, 3111], + "proof_lines": [3078, 3111], + "status": "RED", + "blocking": true, + "dependencies": ["C4", "C5", "C10"], + "first_downstream_use": "Theorem 1 and abstract.", + "issue": "The union-bound intersection and subtraction are correct. The conclusion remains conditional on Proposition 9.2. The printed constant is valid but unnecessarily weakened if the blocking theorem is eventually closed.", + "repair": "After closure, replace the /32 theorem by the phase-resolved /8 theorem and the uniform coefficient (log 2)^2/8*log(1000/639)." + } + ] +} diff --git a/625/experiments/check_line_by_line_audit.py b/625/experiments/check_line_by_line_audit.py new file mode 100644 index 00000000..01a7d3ce --- /dev/null +++ b/625/experiments/check_line_by_line_audit.py @@ -0,0 +1,261 @@ +#!/usr/bin/env python3 +"""Check coverage and internal consistency of the Erdős 625 literal audit. + +The checker validates source SHA, exact theorem ranges, status classifications, +known source defects, and human-audit coverage. It is not a mathematical proof. +""" + +from __future__ import annotations + +import hashlib +import json +import re +from collections import Counter +from pathlib import Path +from typing import Any + + +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / "625/arxiv/main.tex" +AUDIT = ROOT / "625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md" +MANIFEST = ROOT / "625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json" + +BOXED_IDS = { + "T1", + "L2.1", + "L3.1", + "L5.1", + "L6.1", + "L6.2", + "L7.1", + "L8.1", + "L8.2", + "L8.3", + "L9.1", + "P9.2", + "L10.1", + "L10.2", +} + +EXPECTED_STATUS = { + "T1": "RED", + "L2.1": "GREEN", + "L3.1": "GREEN-REWRITE", + "L5.1": "GREEN-REWRITE", + "L6.1": "GREEN", + "L6.2": "GREEN", + "L7.1": "GREEN-REWRITE", + "L8.1": "GREEN-REWRITE", + "L8.2": "GREEN-REWRITE", + "L8.3": "RED", + "L9.1": "SUPERSEDED", + "P9.2": "RED", + "L10.1": "GREEN", + "L10.2": "GREEN", +} + +EXPECTED_BEGIN = { + "T1": 119, + "L2.1": 295, + "L3.1": 495, + "L5.1": 860, + "L6.1": 1354, + "L6.2": 1445, + "L7.1": 1651, + "L8.1": 2053, + "L8.2": 2151, + "L8.3": 2233, + "L9.1": 2550, + "P9.2": 2832, + "L10.1": 2903, + "L10.2": 2968, +} + +EXPECTED_PROOF_BEGIN = { + "L2.1": 324, + "L3.1": 563, + "L5.1": 871, + "L6.1": 1385, + "L6.2": 1484, + "L7.1": 1667, + "L8.1": 2081, + "L8.2": 2171, + "L8.3": 2245, + "L9.1": 2567, + "P9.2": 2844, + "L10.1": 2914, + "L10.2": 2991, +} + +ALLOWED_STATUS = { + "GREEN", + "GREEN-REWRITE", + "AMBER", + "RED", + "TYPO/EDITORIAL", + "SUPERSEDED", +} + +REQUIRED_TAGS = { + "0.1", + "2.2", + "3.7", + "5.3", + "5.11", + "5.20", + "6.4", + "6.8", + "7.7", + "8.8", + "8.16", + "8.21", + "8.30", + "9.2", + "9.3", + "9.23", + "10.3", + "10.5", + "10.13", + "11.1", +} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def boxed_token(item_id: str) -> str: + if item_id == "T1": + return "Theorem 1" + if item_id == "P9.2": + return "Proposition 9.2" + if item_id.startswith("L"): + return f"Lemma {item_id[1:]}" + raise RuntimeError(f"unknown boxed id: {item_id}") + + +def git_blob_sha(raw: bytes) -> str: + return hashlib.sha1(f"blob {len(raw)}\0".encode("ascii") + raw).hexdigest() + + +def source_range(lines: list[str], bounds: list[int]) -> str: + require(len(bounds) == 2, f"invalid range: {bounds}") + start, end = bounds + require(1 <= start <= end <= len(lines), f"out-of-range source span: {bounds}") + return "\n".join(lines[start - 1 : end]) + + +def load_manifest() -> dict[str, Any]: + data = json.loads(MANIFEST.read_text(encoding="utf-8")) + require(isinstance(data.get("items"), list), "manifest items missing") + return data + + +def check_manifest(manifest: dict[str, Any], raw: bytes, lines: list[str]) -> Counter[str]: + require(manifest["source"] == "625/arxiv/main.tex", "manifest source mismatch") + require(manifest["source_blob_sha"] == git_blob_sha(raw), "stale source blob SHA") + items = manifest["items"] + ids = [item["id"] for item in items] + require(len(ids) == len(set(ids)), "duplicate manifest ids") + by_id = {item["id"]: item for item in items} + require(BOXED_IDS <= set(by_id), "boxed statement coverage incomplete") + + for item in items: + item_id = item["id"] + require(item["status"] in ALLOWED_STATUS, f"{item_id}: invalid status") + require(isinstance(item["blocking"], bool), f"{item_id}: invalid blocking flag") + require(item["issue"] and item["repair"], f"{item_id}: empty issue/repair") + statement_text = source_range(lines, item["statement_lines"]) + source_range(lines, item["proof_lines"]) + if item_id in BOXED_IDS: + require(boxed_token(item_id) in statement_text, f"{item_id}: identifier not in range") + + for item_id, expected in EXPECTED_STATUS.items(): + require(by_id[item_id]["status"] == expected, f"{item_id}: status drift") + require( + by_id[item_id]["statement_lines"][0] == EXPECTED_BEGIN[item_id], + f"{item_id}: statement line drift", + ) + + for item_id, proof_begin in EXPECTED_PROOF_BEGIN.items(): + require( + by_id[item_id]["proof_lines"][0] == proof_begin, + f"{item_id}: proof line drift", + ) + head = source_range(lines, [proof_begin, min(proof_begin + 3, len(lines))]) + require("Proof" in head or "\\begin{proof}" in head, f"{item_id}: proof marker absent") + + red_boxed = {item_id for item_id in BOXED_IDS if by_id[item_id]["status"] == "RED"} + require(red_boxed == {"T1", "L8.3", "P9.2"}, f"unexpected RED set: {red_boxed}") + require( + manifest["single_blocking_chain"] + == ["Lemma 8.3", "Proposition 9.2", "Theorem 1"], + "blocking chain drift", + ) + return Counter(item["status"] for item in items) + + +def check_source(text: str) -> None: + tags = re.findall(r"\\tag\{([^}]+)\}", text) + duplicates = [tag for tag, count in Counter(tags).items() if count > 1] + require(not duplicates, f"duplicate equation tags: {duplicates}") + require(REQUIRED_TAGS <= set(tags), f"missing required tags: {sorted(REQUIRED_TAGS - set(tags))}") + require("2^\\ell_\\bullet" in text, "known Section 7 typo absent; refresh audit") + require("2^{\\ell_\\bullet}" not in text, "source typo was fixed without refreshing audit") + require(r"We prove that, for \(G_n\sim G(n,1/2)\)" in text, "abstract claim changed") + require("3a/4+O(1)" in text, "imprecise Section VIII range changed") + + +def check_audit(audit: str, manifest: dict[str, Any]) -> None: + markers = ( + "literal line-by-line and theorem-by-theorem audit", + "There is one submission-blocking chain", + "Lemma 8.3", + "Proposition 9.2", + "Theorem 1", + "2^\\ell_\\bullet", + "matching-restriction", + "Acceptance gates before changing theorem status", + "The current canonical TeX is nevertheless not ready to assert Theorem 1", + "**Theorem 1:** RED", + ) + missing = [marker for marker in markers if marker not in audit] + require(not missing, f"audit markers missing: {missing}") + + for item in manifest["items"]: + start, end = item["statement_lines"] + require( + f"{start}--{end}" in audit or f"{start}–{end}" in audit, + f"audit range absent for {item['id']}", + ) + if item["id"] in BOXED_IDS: + require(boxed_token(item["id"]) in audit, f"audit identifier absent for {item['id']}") + + +def main() -> None: + for path in (SOURCE, AUDIT, MANIFEST): + require(path.is_file(), f"missing file: {path}") + + raw = SOURCE.read_bytes() + text = raw.decode("utf-8") + lines = text.splitlines() + audit = AUDIT.read_text(encoding="utf-8") + manifest = load_manifest() + + require(len(lines) >= 3100, f"canonical source unexpectedly short: {len(lines)}") + counts = check_manifest(manifest, raw, lines) + check_source(text) + check_audit(audit, manifest) + + print("ERDOS 625 LINE-BY-LINE AUDIT CHECK: PASS") + print(f" source lines: {len(lines)}") + print(f" audited items: {len(manifest['items'])}") + print(f" statuses: {dict(sorted(counts.items()))}") + print(f" source blob: {git_blob_sha(raw)}") + print(" RED boxed chain: Lemma 8.3 -> Proposition 9.2 -> Theorem 1") + print(" scope: audit coverage/status consistency only") + + +if __name__ == "__main__": + main() diff --git a/625/experiments/extract_line_by_line_audit_map.py b/625/experiments/extract_line_by_line_audit_map.py new file mode 100644 index 00000000..6968a6e4 --- /dev/null +++ b/625/experiments/extract_line_by_line_audit_map.py @@ -0,0 +1,260 @@ +#!/usr/bin/env python3 +"""Generate a mechanical source map for the canonical Erdős 625 TeX. + +This standard-library script inventories boxed statements, proof ranges, +tagged displays, labels, references, and known audit-risk patterns. It does not +make mathematical truth judgments. +""" + +from __future__ import annotations + +import argparse +import json +import re +from dataclasses import asdict, dataclass +from pathlib import Path + + +BOX_RE = re.compile( + r"\\begin\{(?Presultbox|lemmabox|propositionbox)\}" + r"\{(?P[^}]*)\}" +) +TAG_RE = re.compile(r"\\tag\{([^}]+)\}") +LABEL_RE = re.compile(r"\\label\{([^}]+)\}") +REF_RE = re.compile(r"\\(?:eqref|ref|autoref)\{([^}]+)\}") +PROOF_RE = re.compile(r"\\(?:paragraph\{Proof[^}]*\}|begin\{proof\})") +SECTION_RE = re.compile(r"\\(?:section\*?|subsection\*?)\{") + + +@dataclass(frozen=True) +class Statement: + kind: str + title: str + statement_start: int + statement_end: int + proof_start: int | None + proof_end: int | None + + +@dataclass(frozen=True) +class Display: + tag: str + line: int + preview: str + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def strip_tex(line: str) -> str: + line = re.sub(r"%.*", "", line) + line = re.sub(r"\\[A-Za-z@]+\*?(?:\[[^]]*\])?", " ", line) + line = line.replace("{", " ").replace("}", " ") + return re.sub(r"\s+", " ", line).strip() + + +def find_environment_end(lines: list[str], start: int, kind: str) -> int: + token = f"\\end{{{kind}}}" + for index in range(start, len(lines)): + if token in lines[index]: + return index + 1 + raise RuntimeError(f"unclosed {kind} environment at line {start + 1}") + + +def find_proof( + lines: list[str], statement_end: int, next_statement_start: int | None +) -> tuple[int | None, int | None]: + limit = next_statement_start - 1 if next_statement_start else len(lines) + proof_start: int | None = None + for index in range(statement_end, limit): + if PROOF_RE.search(lines[index]): + proof_start = index + 1 + break + if SECTION_RE.search(lines[index]) or BOX_RE.search(lines[index]): + break + if proof_start is None: + return None, None + for index in range(proof_start - 1, limit): + if "\\square" in lines[index] or "\\end{proof}" in lines[index]: + return proof_start, index + 1 + return proof_start, limit + + +def collect_statements(lines: list[str]) -> list[Statement]: + raw: list[tuple[str, str, int, int]] = [] + for index, line in enumerate(lines): + match = BOX_RE.search(line) + if match: + kind = match.group("kind") + raw.append( + ( + kind, + match.group("title").strip(), + index + 1, + find_environment_end(lines, index, kind), + ) + ) + result: list[Statement] = [] + for position, (kind, title, start, end) in enumerate(raw): + next_start = raw[position + 1][2] if position + 1 < len(raw) else None + proof_start, proof_end = find_proof(lines, end, next_start) + result.append(Statement(kind, title, start, end, proof_start, proof_end)) + return result + + +def collect_displays(lines: list[str]) -> list[Display]: + displays: list[Display] = [] + for index, line in enumerate(lines, start=1): + for match in TAG_RE.finditer(line): + lo = max(0, index - 4) + hi = min(len(lines), index + 3) + preview = " ".join( + part for part in (strip_tex(item) for item in lines[lo:hi]) if part + )[:180] + displays.append(Display(match.group(1), index, preview)) + return displays + + +def collect_occurrences(lines: list[str], pattern: re.Pattern[str]) -> dict[str, list[int]]: + result: dict[str, list[int]] = {} + for index, line in enumerate(lines, start=1): + for match in pattern.finditer(line): + result.setdefault(match.group(1), []).append(index) + return result + + +def collect_flags(lines: list[str], statements: list[Statement]) -> list[dict[str, object]]: + patterns = ( + ("UNCONDITIONAL_CLAIM", re.compile(r"\bWe prove\b")), + ("KNOWN_TEX_TYPO", re.compile(r"2\^\\ell_\\bullet")), + ("DECIMAL_CERTIFICATE", re.compile(r"\b0\.\d{3,}")), + ("IMPRECISE_FINITE_RANGE", re.compile(r"[+\-]O\(1\)")), + ("ASYMPTOTIC_PLACEHOLDER", re.compile(r"o\(1\)")), + ) + flags: list[dict[str, object]] = [] + for index, line in enumerate(lines, start=1): + visible = re.sub(r"%.*", "", line) + for name, pattern in patterns: + if pattern.search(visible): + flags.append({"kind": name, "line": index, "preview": strip_tex(visible)}) + for statement in statements: + if statement.proof_start is None: + flags.append( + { + "kind": "NO_LOCAL_PROOF", + "line": statement.statement_start, + "preview": statement.title, + } + ) + return flags + + +def render( + source: Path, + lines: list[str], + statements: list[Statement], + displays: list[Display], + labels: dict[str, list[int]], + references: dict[str, list[int]], + flags: list[dict[str, object]], +) -> str: + duplicate_labels = {key: value for key, value in labels.items() if len(value) > 1} + missing_references = sorted(set(references) - set(labels)) + tag_counts: dict[str, int] = {} + for display in displays: + tag_counts[display.tag] = tag_counts.get(display.tag, 0) + 1 + duplicate_tags = sorted(tag for tag, count in tag_counts.items() if count > 1) + + out = [ + "# Generated source map for the Erdős 625 canonical TeX", + "", + f"- Source: `{source.as_posix()}`", + f"- Lines: `{len(lines)}`", + f"- Boxed statements: `{len(statements)}`", + f"- Tagged displays: `{len(displays)}`", + "", + "> Mechanical coverage only; mathematical verdicts are in the human audit.", + "", + "## Boxed statement ledger", + "", + "| # | Kind | Statement lines | Proof lines | Title |", + "|---:|---|---:|---:|---|", + ] + for number, statement in enumerate(statements, start=1): + proof = ( + f"{statement.proof_start}–{statement.proof_end}" + if statement.proof_start and statement.proof_end + else "—" + ) + out.append( + f"| {number} | `{statement.kind}` | " + f"{statement.statement_start}–{statement.statement_end} | {proof} | " + f"{statement.title} |" + ) + + out.extend(["", "## Tagged-display ledger", "", "| Tag | Line | Preview |", "|---|---:|---|"]) + for display in displays: + out.append(f"| `{display.tag}` | {display.line} | {display.preview.replace('|', '/') } |") + + out.extend( + [ + "", + "## Mechanical consistency", + "", + f"- Duplicate labels: `{json.dumps(duplicate_labels, sort_keys=True)}`", + f"- Duplicate tags: `{json.dumps(duplicate_tags)}`", + f"- References to missing labels: `{json.dumps(missing_references)}`", + "", + "## Audit-risk flags", + "", + "| Kind | Line | Preview |", + "|---|---:|---|", + ] + ) + for flag in flags: + preview = str(flag["preview"]).replace("|", "/") + out.append(f"| `{flag['kind']}` | {flag['line']} | {preview} |") + + out.extend( + [ + "", + "## Machine-readable statement manifest", + "", + "```json", + json.dumps([asdict(statement) for statement in statements], indent=2), + "```", + "", + ] + ) + return "\n".join(out) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("source", nargs="?", type=Path, default=Path("625/arxiv/main.tex")) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + + lines = args.source.read_text(encoding="utf-8").splitlines() + statements = collect_statements(lines) + displays = collect_displays(lines) + labels = collect_occurrences(lines, LABEL_RE) + references = collect_occurrences(lines, REF_RE) + flags = collect_flags(lines, statements) + output = render(args.source, lines, statements, displays, labels, references, flags) + + require(len(statements) >= 14, "too few boxed statements found") + require(any(statement.title == "Theorem 1" for statement in statements), "Theorem 1 absent") + require(any(statement.title.startswith("Proposition 9.2") for statement in statements), "Proposition 9.2 absent") + + if args.output: + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text(output, encoding="utf-8") + else: + print(output) + + +if __name__ == "__main__": + main()