diff --git a/.github/workflows/erdos625-line-by-line-audit.yml b/.github/workflows/erdos625-line-by-line-audit.yml new file mode 100644 index 00000000..212a2bfc --- /dev/null +++ b/.github/workflows/erdos625-line-by-line-audit.yml @@ -0,0 +1,86 @@ +name: Erdős 625 line-by-line theorem audit + +on: + pull_request: + paths: + - "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/extract_line_by_line_audit_map.py" + - "625/experiments/check_line_by_line_audit.py" + - ".github/workflows/erdos625-line-by-line-audit.yml" + workflow_dispatch: + +concurrency: + group: erdos625-line-audit-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + generate-source-map: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Compile the source-map extractor + run: python -m py_compile 625/experiments/extract_line_by_line_audit_map.py + - name: Generate the exact source map + run: | + python 625/experiments/extract_line_by_line_audit_map.py \ + 625/arxiv/main.tex \ + --output /tmp/ERDOS625_GENERATED_SOURCE_MAP.md + - name: Validate basic coverage + run: | + python - <<'PY' + from pathlib import Path + source = Path("625/arxiv/main.tex").read_text(encoding="utf-8").splitlines() + audit = Path("/tmp/ERDOS625_GENERATED_SOURCE_MAP.md").read_text(encoding="utf-8") + if len(source) < 3000: + raise SystemExit(f"unexpectedly short canonical TeX: {len(source)} lines") + required = ( + "Boxed theorem/lemma/proposition ledger", + "Tagged-display ledger", + "Mechanical consistency checks", + "Audit-risk flags", + "Theorem 1", + "Lemma 3.1", + "Lemma 5.1", + "Lemma 6.1", + "Lemma 6.2", + "Lemma 7.1", + "Lemma 8.1", + "Lemma 8.2", + "Lemma 8.3", + "Lemma 9.1", + "Proposition 9.2", + "Lemma 10.1", + "Lemma 10.2", + ) + missing = [token for token in required if token not in audit] + if missing: + raise SystemExit(f"source-map coverage missing: {missing}") + print(f"source lines: {len(source)}") + print("source-map coverage markers passed") + PY + - name: Upload generated source map + uses: actions/upload-artifact@v4 + with: + name: erdos625-generated-source-map + path: /tmp/ERDOS625_GENERATED_SOURCE_MAP.md + if-no-files-found: error + + validate-human-audit: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Validate audit when present + shell: bash + run: | + if [[ -f 625/experiments/check_line_by_line_audit.py ]]; then + python -m py_compile 625/experiments/check_line_by_line_audit.py + python 625/experiments/check_line_by_line_audit.py + python -O 625/experiments/check_line_by_line_audit.py + else + echo "Human audit checker not yet present; source-map job remains authoritative." + fi diff --git a/.github/workflows/erdos625-sharp-deficit-product.yml b/.github/workflows/erdos625-sharp-deficit-product.yml index d04aead0..1e30719c 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,27 @@ 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 + run: python 625/experiments/check_line_by_line_audit.py + - name: Run audit checker with optimization + run: python -O 625/experiments/check_line_by_line_audit.py + - name: Generate exact source-map artifact + 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 + uses: actions/upload-artifact@v4 + with: + name: erdos625-generated-source-map + path: /tmp/ERDOS625_GENERATED_SOURCE_MAP.md + if-no-files-found: error 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..0b25830e --- /dev/null +++ b/625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md @@ -0,0 +1,792 @@ +# 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` +**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--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 295--322 + +- 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--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: lines 495--561 + +- 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--80 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 82--95 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. + +### Root displacement and midpoint profile: lines 1123--1307 + +- **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. + +### Constant audit + +The text loses more constant than required: + +1. (5.11) gives the phase coefficient \((\log2)^2/4\); +2. midpoint placement retains one half, giving \((\log2)^2/8\); +3. integer rounding and amplification are lower order and do not require + another fixed halving. + +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. +\] + +## 9. Lemma 6.1: lines 1354--1428 — **GREEN** + +### Statement + +The normalized sign factor is + +\[ + 2^{W+c(H)-|V(H)|} + =\left(\prod_{a,b}g(r_{ab})\right)2^{\beta(H)}. +\] + +### Proof ledger + +- **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. + +## 10. Lemma 6.2: lines 1445--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. + +## 11. Section 7 and Lemma 7.1: lines 1525--1935 — **GREEN-REWRITE** + +### Exact identities: lines 1525--1649 + +- 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}`. This is TYPO/EDITORIAL. +- Equations (7.3)--(7.6) follow by exact factorial cancellation and one-coordinate + ratios. They are mathematically correct. + +### Lemma 7.1 statement: lines 1651--1659 + +The target \(\sum_\ell D(\ell)=1+o(1)\) is exactly what endpoint transportation +needs. + +### Empty corner: lines 1667--1704 + +- The lower bound on \(\mu_{u_i}(n)\) gives + \(\Xi_{\mathrm{empty}}=o(1)\). +- If selected mass is at most \(\eta n\), the changing ambient vertex count costs + at most a small power of \(\log n\). +- Iterating (7.4) in any order gives a product of exponential-series terms, and + the 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 appear correct, but they 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 when the selected mass is away from both + corners. + +### Full corner: lines 1907--1935 + +- The shift estimates give \(\mu_{u_i}(n)\le n^{6+o(1)}\) uniformly over the four + sizes. +- For residual mass at most \(n/32\), the factor \(32^{-u_i}\) supplies + \(n^{-10+o(1)}\), making the reverse recurrence strictly decreasing. +- Division by the exponentially large complete signed first moment makes the + entire full corner negligible. + +**Repair:** fix (7.2), replace decimal central-rate checks with the exact +certificate, and bind every \(o(1)\) to a deterministic phase-uniform sequence. + +## 12. Section 8 up to Lemma 8.2: lines 1937--2228 + +### Canonical high support: lines 1937--2052 — **GREEN-REWRITE** + +- A cell above \(R_0=\lfloor u_{\max}/2\rfloor\) is unique in its row and column, + so high cells form a matching. +- Selecting exact high-cell stub pairs gives (8.3). +- Conditional cancellation with the residual matching recovers the exact + overlap law (6.2). +- The endpoint reference weights \(W(L)\) and one-sided diagonal weights \(D(r)\) + have now been independently normalized in the formal stack. + +The prose should distinguish clearly between: + +1. a block-level matching support; +2. a physical partial stub matching in a selected cell; +3. an aggregate fibre sum. + +### Lemma 8.1: lines 2053--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). +- 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. + +### Lemma 8.2: lines 2151--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. +- The number of margin vectors contributes only a polynomial factor. +- 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\). Use that route in Version 2. + +## 13. Lemma 8.3: lines 2233--2490 — **RED** + +This is the only independent submission blocker. + +### Statement: lines 2233--2243 + +The desired conclusion is exactly the necessary bare-skeleton estimate. The +problem is not the target but the finite identification used to reach it. + +### Proof introduction: lines 2245--2263 + +The near/middle charging narrative announces an objectwise completion picture. +That picture must be interpreted only after summing physical fibres: 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. +- The high/middle inequalities are arithmetically correct. +- Replacing selected multiplicities by full endpoint multiplicities produces a + valid block-level reference table. +- What is missing is a weight-preserving finite theorem connecting the actual + physical high-skeleton 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. This is the precise gap. + +### Steps III--IV, lines 2370--2469 + +- The joint threshold estimate is applied before constraints are relaxed, so + the upper-bound direction is preserved. +- The finite sums use ranges such as \(3a/4+O(1)\), which are not literal finite + index sets and must be replaced by exact floor/ceiling bounds. +- The large-residual quadratic exponent is negative on the stated interval. +- The small-residual pointwise bound is conservative. +- Step IV pays residual local and cycle factors even though the Section VIII + contract says those factors are deferred. This may still be an upper bound, + because the inserted factors are at least one, but it obscures the + factorization and creates apparent double charging. + +### 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 + +For a block support \(P\), endpoint minima \(m_e\), and deficits \(h_e\), prove +an exact finite decomposition with aggregate weight + +\[ + w(P,m-h)= + \frac{\prod_e(s_e)_{m_e-h_e}(t_e)_{m_e-h_e}} + {(n)_{\sum_e(m_e-h_e)}\prod_e(m_e-h_e)!} + \prod_e g(m_e-h_e). +\] + +Then + +\[ + \frac{w(P,m-h)}{w_{\mathrm{full}}(P)} + \le + \prod_e n^{h_e}R_{m_e,d_e}(h_e) +\] + +uses the local ratio cell by cell and the global denominator only once. + +The checked sharper arithmetic gives, whenever \(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. +``` + +## 20. 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, not before, + 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-level typo, theorem coefficient, Lean status, + and reproducibility language are synchronized. + +## 21. 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 the 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 already 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..76aa4547 --- /dev/null +++ b/625/experiments/check_line_by_line_audit.py @@ -0,0 +1,307 @@ +#!/usr/bin/env python3 +"""Validate the literal theorem-by-theorem audit of the Erdős 625 TeX. + +This checker verifies coverage, exact source ranges, status consistency, and +known source defects. It does not prove any mathematical theorem. +""" + +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" + +ALLOWED_STATUSES = { + "GREEN", + "GREEN-REWRITE", + "AMBER", + "RED", + "TYPO/EDITORIAL", + "SUPERSEDED", +} + +REQUIRED_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_BOXED_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_LINES = { + "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_STARTS = { + "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, +} + +REQUIRED_EQUATION_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 git_blob_sha(raw: bytes) -> str: + header = f"blob {len(raw)}\0".encode("ascii") + return hashlib.sha1(header + raw).hexdigest() + + +def load_manifest() -> dict[str, Any]: + data = json.loads(MANIFEST.read_text(encoding="utf-8")) + require(isinstance(data, dict), "manifest root must be an object") + require(isinstance(data.get("items"), list), "manifest items must be a list") + return data + + +def line_slice(lines: list[str], start: int, end: int) -> str: + require(1 <= start <= end <= len(lines), f"invalid source range {start}-{end}") + return "\n".join(lines[start - 1 : end]) + + +def validate_manifest_against_source( + manifest: dict[str, Any], source_raw: bytes, source_lines: list[str] +) -> Counter[str]: + require(manifest.get("source") == "625/arxiv/main.tex", "manifest source mismatch") + require( + manifest.get("source_blob_sha") == git_blob_sha(source_raw), + "manifest source blob SHA is stale", + ) + + items = manifest["items"] + ids = [item.get("id") for item in items] + require(all(isinstance(item_id, str) and item_id for item_id in ids), "invalid item id") + require(len(ids) == len(set(ids)), "duplicate item ids in manifest") + item_by_id = {item["id"]: item for item in items} + + require(REQUIRED_BOXED_IDS <= set(item_by_id), "boxed theorem coverage is incomplete") + + for item in items: + item_id = item["id"] + status = item.get("status") + require(status in ALLOWED_STATUSES, f"{item_id}: invalid status {status!r}") + require(isinstance(item.get("blocking"), bool), f"{item_id}: blocking must be bool") + require(item.get("issue"), f"{item_id}: missing issue field") + require(item.get("repair"), f"{item_id}: missing repair field") + statement_range = item.get("statement_lines") + proof_range = item.get("proof_lines") + require( + isinstance(statement_range, list) and len(statement_range) == 2, + f"{item_id}: malformed statement range", + ) + require( + isinstance(proof_range, list) and len(proof_range) == 2, + f"{item_id}: malformed proof range", + ) + statement_text = line_slice(source_lines, *statement_range) + line_slice(source_lines, *proof_range) + if item_id in REQUIRED_BOXED_IDS: + require( + item["title"] in statement_text, + f"{item_id}: title absent from statement range", + ) + + for item_id, expected_status in EXPECTED_BOXED_STATUS.items(): + require( + item_by_id[item_id]["status"] == expected_status, + f"{item_id}: expected {expected_status}, found {item_by_id[item_id]['status']}", + ) + require( + item_by_id[item_id]["statement_lines"][0] == EXPECTED_BEGIN_LINES[item_id], + f"{item_id}: statement begin line drifted", + ) + + for item_id, proof_start in EXPECTED_PROOF_STARTS.items(): + require( + item_by_id[item_id]["proof_lines"][0] == proof_start, + f"{item_id}: proof begin line drifted", + ) + proof_head = line_slice(source_lines, proof_start, min(proof_start + 3, len(source_lines))) + require( + "Proof" in proof_head or "\\begin{proof}" in proof_head, + f"{item_id}: proof marker absent at recorded start", + ) + + theorem_blockers = { + item_id + for item_id in REQUIRED_BOXED_IDS + if item_by_id[item_id]["status"] == "RED" + } + require( + theorem_blockers == {"T1", "L8.3", "P9.2"}, + f"unexpected boxed RED set: {sorted(theorem_blockers)}", + ) + require( + manifest.get("single_blocking_chain") + == ["Lemma 8.3", "Proposition 9.2", "Theorem 1"], + "blocking chain changed unexpectedly", + ) + + return Counter(item["status"] for item in items) + + +def validate_source_invariants(source_text: str) -> None: + tags = re.findall(r"\\tag\{([^}]+)\}", source_text) + counts = Counter(tags) + duplicates = sorted(tag for tag, count in counts.items() if count > 1) + require(not duplicates, f"duplicate equation tags: {duplicates}") + missing_tags = sorted(REQUIRED_EQUATION_TAGS - set(tags)) + require(not missing_tags, f"required equation tags missing: {missing_tags}") + + require("2^\\ell_\\bullet" in source_text, "known equation (7.2) typo no longer present") + require( + "2^{\\ell_\\bullet}" not in source_text, + "canonical source was silently repaired without updating this audit", + ) + require( + r"We prove that, for \(G_n\sim G(n,1/2)\)" in source_text, + "audit-safe abstract may have replaced the canonical claim; refresh audit", + ) + require("3a/4+O(1)" in source_text, "imprecise Section VIII range marker disappeared") + + +def validate_audit_text(audit_text: str, manifest: dict[str, Any]) -> None: + required_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", + "three-quarter", + "matching-restriction", + "Acceptance gates before changing theorem status", + ) + missing = [marker for marker in required_markers if marker not in audit_text] + require(not missing, f"audit markdown missing markers: {missing}") + + for item in manifest["items"]: + start, end = item["statement_lines"] + range_tokens = (f"{start}--{end}", f"{start}–{end}") + require( + any(token in audit_text for token in range_tokens), + f"audit markdown omits source range for {item['id']}", + ) + if item["id"] in REQUIRED_BOXED_IDS: + require( + item["title"] in audit_text, + f"audit markdown omits {item['title']}", + ) + + require( + "The current canonical TeX is nevertheless not ready to assert Theorem 1" + in audit_text, + "final status boundary is missing", + ) + require("**Theorem 1:** RED" in audit_text, "final theorem RED classification is missing") + + +def main() -> None: + for path in (SOURCE, AUDIT, MANIFEST): + require(path.is_file(), f"missing required file: {path}") + + source_raw = SOURCE.read_bytes() + source_text = source_raw.decode("utf-8") + source_lines = source_text.splitlines() + audit_text = AUDIT.read_text(encoding="utf-8") + manifest = load_manifest() + + require(len(source_lines) >= 3100, f"canonical TeX unexpectedly short: {len(source_lines)}") + status_counts = validate_manifest_against_source(manifest, source_raw, source_lines) + validate_source_invariants(source_text) + validate_audit_text(audit_text, manifest) + + print("ERDOS 625 LINE-BY-LINE AUDIT CHECK: PASS") + print(f" canonical source lines: {len(source_lines)}") + print(f" audited items: {len(manifest['items'])}") + print(f" status counts: {dict(sorted(status_counts.items()))}") + print(f" source blob: {git_blob_sha(source_raw)}") + print(" boxed RED chain: Lemma 8.3 -> Proposition 9.2 -> Theorem 1") + print(" scope: coverage and status consistency; not a proof of the mathematics") + + +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 index c1b0730e..aceaa897 100644 --- a/625/experiments/extract_line_by_line_audit_map.py +++ b/625/experiments/extract_line_by_line_audit_map.py @@ -1 +1,395 @@ -x \ No newline at end of file +#!/usr/bin/env python3 +"""Extract a deterministic line-by-line audit map from the Erdős 625 TeX. + +The script is standard-library only. It does not judge mathematical truth. +It identifies the exact source ranges of sections, boxed statements, proofs, +tagged displays, labels, and selected audit-risk patterns so that a human audit +cannot silently skip a theorem or proof transition. +""" + +from __future__ import annotations + +import argparse +import json +import re +from dataclasses import asdict, dataclass +from pathlib import Path + + +STATEMENT_BEGIN_RE = re.compile( + r"\\begin\{(?Presultbox|lemmabox|propositionbox)\}" + r"\{(?P.*)\}\s*$" +) +SECTION_RE = re.compile(r"\\(?P<kind>section\*?|subsection\*?)\{(?P<title>.*)\}") +DISPLAY_HEADING_RE = re.compile(r"\\displayheading\{(?P<title>.*)\}") +PARAGRAPH_RE = re.compile(r"\\paragraph\{(?P<title>.*)\}") +TAG_RE = re.compile(r"\\tag\{(?P<tag>[^}]+)\}") +LABEL_RE = re.compile(r"\\label\{(?P<label>[^}]+)\}") +REFERENCE_RE = re.compile(r"\\(?:eqref|ref|autoref)\{(?P<label>[^}]+)\}") +CITATION_RE = re.compile(r"\\cite[tp]?\s*(?:\[[^]]*\])?\{(?P<keys>[^}]+)\}") + + +@dataclass(frozen=True) +class RangeItem: + kind: str + title: str + start_line: int + end_line: int + + +@dataclass(frozen=True) +class Statement: + kind: str + title: str + start_line: int + end_line: int + label: str | None + proof_start: int | None + proof_end: int | None + + +@dataclass(frozen=True) +class Equation: + tag: str + start_line: int + end_line: int + preview: str + + +def normalize_tex(text: str) -> str: + text = re.sub(r"%.*", "", text) + text = re.sub(r"\\(?:textup|textbf|emph|texorpdfstring)\{([^{}]*)\}", r"\1", text) + text = re.sub(r"\\[A-Za-z@]+\*?(?:\[[^]]*\])?", " ", text) + text = text.replace("{", " ").replace("}", " ") + return re.sub(r"\s+", " ", text).strip() + + +def display_start_at(lines: list[str], tag_index: int) -> int: + depth = 0 + for index in range(tag_index, -1, -1): + line = lines[index] + if "\\]" in line: + depth += line.count("\\]") + if "\\[" in line: + if depth == 0: + return index + 1 + depth -= line.count("\\[") + if re.search(r"\\begin\{(?:equation\*?|align\*?|gather\*?|multline\*?)\}", line): + return index + 1 + return tag_index + 1 + + +def display_end_at(lines: list[str], tag_index: int) -> int: + for index in range(tag_index, len(lines)): + line = lines[index] + if "\\]" in line or re.search( + r"\\end\{(?:equation\*?|align\*?|gather\*?|multline\*?)\}", line + ): + return index + 1 + if index > tag_index and STATEMENT_BEGIN_RE.search(line): + break + return tag_index + 1 + + +def next_nonempty_preview(lines: list[str], start: int, end: int) -> str: + pieces: list[str] = [] + for line in lines[start - 1 : end]: + cleaned = normalize_tex(line) + if cleaned: + pieces.append(cleaned) + if sum(len(piece) for piece in pieces) >= 150: + break + return " ".join(pieces)[:180] + + +def find_end_environment(lines: list[str], start_index: int, environment: str) -> int: + token = f"\\end{{{environment}}}" + for index in range(start_index + 1, len(lines)): + if token in lines[index]: + return index + 1 + raise RuntimeError(f"unclosed environment {environment} at line {start_index + 1}") + + +def find_statement_label(lines: list[str], start_line: int, end_line: int) -> str | None: + lower = max(0, start_line - 8) + upper = min(len(lines), end_line) + labels: list[str] = [] + for line in lines[lower:upper]: + labels.extend(match.group("label") for match in LABEL_RE.finditer(line)) + return labels[-1] if labels else None + + +def find_proof_range( + lines: list[str], statement_end: int, next_statement_start: int | None +) -> tuple[int | None, int | None]: + search_end = (next_statement_start - 1) if next_statement_start else len(lines) + proof_start: int | None = None + for index in range(statement_end, search_end): + line = lines[index] + paragraph = PARAGRAPH_RE.search(line) + if paragraph and paragraph.group("title").lower().startswith("proof"): + proof_start = index + 1 + break + if "\\begin{proof}" in line: + proof_start = index + 1 + break + if SECTION_RE.search(line) or STATEMENT_BEGIN_RE.search(line): + break + if proof_start is None: + return None, None + for index in range(proof_start - 1, search_end): + line = lines[index] + if "\\square" in line or "\\end{proof}" in line: + return proof_start, index + 1 + if index + 1 > proof_start and SECTION_RE.search(line): + return proof_start, index + return proof_start, search_end + + +def collect_ranges(lines: list[str]) -> list[RangeItem]: + starts: list[tuple[str, str, int]] = [] + for index, line in enumerate(lines, start=1): + section = SECTION_RE.search(line) + if section: + starts.append((section.group("kind"), normalize_tex(section.group("title")), index)) + continue + heading = DISPLAY_HEADING_RE.search(line) + if heading: + starts.append(("displayheading", normalize_tex(heading.group("title")), index)) + continue + paragraph = PARAGRAPH_RE.search(line) + if paragraph: + starts.append(("paragraph", normalize_tex(paragraph.group("title")), index)) + result: list[RangeItem] = [] + for pos, (kind, title, start) in enumerate(starts): + end = starts[pos + 1][2] - 1 if pos + 1 < len(starts) else len(lines) + result.append(RangeItem(kind, title, start, end)) + return result + + +def collect_statements(lines: list[str]) -> list[Statement]: + raw: list[tuple[str, str, int, int]] = [] + for index, line in enumerate(lines): + match = STATEMENT_BEGIN_RE.search(line) + if not match: + continue + kind = match.group("kind") + title = normalize_tex(match.group("title")) + end = find_end_environment(lines, index, kind) + raw.append((kind, title, index + 1, end)) + statements: list[Statement] = [] + for pos, (kind, title, start, end) in enumerate(raw): + next_start = raw[pos + 1][2] if pos + 1 < len(raw) else None + proof_start, proof_end = find_proof_range(lines, end, next_start) + statements.append( + Statement( + kind=kind, + title=title, + start_line=start, + end_line=end, + label=find_statement_label(lines, start, end), + proof_start=proof_start, + proof_end=proof_end, + ) + ) + return statements + + +def collect_equations(lines: list[str]) -> list[Equation]: + equations: list[Equation] = [] + for index, line in enumerate(lines): + for match in TAG_RE.finditer(line): + start = display_start_at(lines, index) + end = display_end_at(lines, index) + equations.append( + Equation( + tag=match.group("tag"), + start_line=start, + end_line=end, + preview=next_nonempty_preview(lines, start, end), + ) + ) + return equations + + +def collect_labels(lines: list[str]) -> dict[str, list[int]]: + result: dict[str, list[int]] = {} + for index, line in enumerate(lines, start=1): + for match in LABEL_RE.finditer(line): + result.setdefault(match.group("label"), []).append(index) + return result + + +def collect_references(lines: list[str]) -> dict[str, list[int]]: + result: dict[str, list[int]] = {} + for index, line in enumerate(lines, start=1): + for match in REFERENCE_RE.finditer(line): + result.setdefault(match.group("label"), []).append(index) + return result + + +def collect_citations(lines: list[str]) -> dict[str, list[int]]: + result: dict[str, list[int]] = {} + for index, line in enumerate(lines, start=1): + for match in CITATION_RE.finditer(line): + for key in match.group("keys").split(","): + result.setdefault(key.strip(), []).append(index) + return result + + +def risk_flags(lines: list[str], statements: list[Statement]) -> list[tuple[str, int, str]]: + flags: list[tuple[str, int, str]] = [] + patterns: tuple[tuple[str, re.Pattern[str]], ...] = ( + ("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_RANGE", re.compile(r"[+\-]O\(1\)")), + ("ASYMPTOTIC_PLACEHOLDER", re.compile(r"\bo\(1\)\b")), + ) + for index, line in enumerate(lines, start=1): + stripped = re.sub(r"%.*", "", line) + for name, pattern in patterns: + if pattern.search(stripped): + flags.append((name, index, normalize_tex(stripped))) + for statement in statements: + if statement.proof_start is None: + flags.append( + ("NO_LOCAL_PROOF", statement.start_line, f"{statement.title}: no following proof block") + ) + return flags + + +def duplicate_values(mapping: dict[str, list[int]]) -> dict[str, list[int]]: + return {key: value for key, value in mapping.items() if len(value) > 1} + + +def render_markdown( + source: Path, + lines: list[str], + ranges: list[RangeItem], + statements: list[Statement], + equations: list[Equation], + labels: dict[str, list[int]], + references: dict[str, list[int]], + citations: dict[str, list[int]], + flags: list[tuple[str, int, str]], +) -> str: + missing_references = sorted(set(references) - set(labels)) + duplicate_labels = duplicate_values(labels) + duplicate_tags = duplicate_values( + {tag: [eq.start_line for eq in equations if eq.tag == tag] for tag in {eq.tag for eq in equations}} + ) + + out: list[str] = [] + out.append("# Generated source map for the Erdős 625 canonical TeX") + out.append("") + out.append(f"- Source: `{source.as_posix()}`") + out.append(f"- Lines: `{len(lines)}`") + out.append(f"- Boxed statements: `{len(statements)}`") + out.append(f"- Tagged displays: `{len(equations)}`") + out.append(f"- Labels: `{len(labels)}`") + out.append(f"- Citation keys used: `{len(citations)}`") + out.append("") + out.append("> This file is a mechanical coverage map, not a mathematical verdict.") + out.append("") + + out.append("## Section and paragraph ranges") + out.append("") + out.append("| Kind | Lines | Heading |") + out.append("|---|---:|---|") + for item in ranges: + out.append(f"| `{item.kind}` | {item.start_line}–{item.end_line} | {item.title or '—'} |") + out.append("") + + out.append("## Boxed theorem/lemma/proposition ledger") + out.append("") + out.append("| # | Kind | Statement lines | Proof lines | Label | Title |") + out.append("|---:|---|---:|---:|---|---|") + for number, statement in enumerate(statements, start=1): + proof = ( + f"{statement.proof_start}–{statement.proof_end}" + if statement.proof_start is not None and statement.proof_end is not None + else "—" + ) + out.append( + f"| {number} | `{statement.kind}` | {statement.start_line}–{statement.end_line} " + f"| {proof} | `{statement.label or '—'}` | {statement.title} |" + ) + out.append("") + + out.append("## Tagged-display ledger") + out.append("") + out.append("| Tag | Lines | Preview |") + out.append("|---|---:|---|") + for equation in equations: + preview = equation.preview.replace("|", "\\|") + out.append(f"| `{equation.tag}` | {equation.start_line}–{equation.end_line} | {preview} |") + out.append("") + + out.append("## Mechanical consistency checks") + out.append("") + out.append(f"- Duplicate labels: `{json.dumps(duplicate_labels, sort_keys=True)}`") + out.append(f"- Duplicate equation tags: `{json.dumps(duplicate_tags, sort_keys=True)}`") + out.append(f"- References to missing labels: `{json.dumps(missing_references)}`") + out.append("") + + out.append("## Audit-risk flags") + out.append("") + out.append("| Class | Line | Source preview |") + out.append("|---|---:|---|") + for name, line, preview in flags: + out.append(f"| `{name}` | {line} | {preview.replace('|', '\\|')} |") + out.append("") + + out.append("## Machine-readable statement manifest") + out.append("") + out.append("```json") + out.append(json.dumps([asdict(statement) for statement in statements], indent=2, sort_keys=True)) + out.append("```") + out.append("") + return "\n".join(out) + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser() + parser.add_argument( + "source", + nargs="?", + type=Path, + default=Path("625/arxiv/main.tex"), + ) + parser.add_argument("--output", type=Path) + return parser.parse_args() + + +def main() -> None: + args = parse_args() + source: Path = args.source + lines = source.read_text(encoding="utf-8").splitlines() + ranges = collect_ranges(lines) + statements = collect_statements(lines) + equations = collect_equations(lines) + labels = collect_labels(lines) + references = collect_references(lines) + citations = collect_citations(lines) + flags = risk_flags(lines, statements) + rendered = render_markdown( + source, + lines, + ranges, + statements, + equations, + labels, + references, + citations, + flags, + ) + if args.output: + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text(rendered, encoding="utf-8") + else: + print(rendered) + + +if __name__ == "__main__": + main()