Isolate verified Section 7 and Section 9 simplifications

[SamPetkov]

Summary

This is a clean follow-up to draft PR #27, created directly from the current main branch. It isolates only two claims that survived a second adversarial review and an independent exact test suite:

1. the Section 7 central partial-diagonal rate can be strengthened from 1/5000 to 1/100 on the same domain;
2. the Section 9 large-residual cycle-to-walk argument can be replaced by a direct restriction-to-residual-edges injection.

No canonical manuscript, PDF, Lean source, or theorem statement is changed.

Mathematical simplification

For the exposed high matching M, restriction

F -> F \ M

is injective on even edge sets. Therefore

sum_F prod_{e in F\M} q_e
  <= sum_{S subset residual} prod_{e in S} q_e
  =  prod_{e notin M} (1 + q_e)
  <= exp(sum_{e notin M} q_e).

Using the corrected one-sided off-matching square-sum inequality and the existing local-increment estimate gives

A(M,j) <= exp(C (U^2 + U^4/m_0)).

In the large-residual regime this is exp(O(N^2)), improving the manuscript's exp(O(N^8)) envelope. The simple-cycle decomposition, residual-walk enumeration, mixed matching-cycle encoding, parameter tau, and term h tau are not needed for this bound.

Files

• 625/proofs/SECTION7_SECTION9_SUPERCHECK.md
• 625/audits/SECTION7_SECTION9_SUPERCHECK.md
• 625/experiments/section7_section9_supercheck.py
• .github/workflows/erdos625-section7-section9-supercheck.yml

Exact verification

The standard-library script uses integer and Fraction arithmetic and raises explicit exceptions under python -O; it does not rely on optimization-sensitive assertions.

Current output:

ERDOS 625 SECTION 7/9 SUPERCHECK: PASS
  central-rate endpoint inequalities: exact Fraction bounds
  residual relations exhausted: 5912
  even edge sets checked: 12561
  square-sum instances checked: 613711

The graph test exhausts every partial matching and every residual relation for K_{2,2}, K_{2,3}, and K_{3,3}, with two rational weight systems. The Section 7 endpoint signs use rigorous rational logarithm bounds from the atanh series rather than floating-point evaluation.

The new focused workflow runs:

• python -m py_compile;
• normal execution;
• execution under python -O.

Both Markdown files were also parsed locally with Pandoc.

Deliberate scope boundary

This PR does not promote the broader PR #27 claims concerning:

• the complete Section 8 high-skeleton summation;
• theorem-constant improvements;
• new entropy certificates;
• the three-size profile;
• non-midpoint placement;
• literature-dependent corollaries.

It still depends on the canonical manuscript's threshold expansion through equation (9.12) and its local estimate through equation (9.13). It does not prove Proposition 9.2 or Erdos625Statement by itself.

[SamPetkov]

Super-check verdict for this isolated PR: PASS within the stated scope.

The direct mathematical review found no counterexample to either isolated claim. The exact workflow also passed all three gates on head 9e40ff52bee811ca073ccff66dd5f5afa8be75ce: bytecode compilation, normal execution, and execution under python -O.

The strongest verified conclusion here is the one-sided large-residual envelope

A(M,j) <= exp(C (U^2 + U^4/m_0)) = exp(O(N^2)),

conditional on the canonical threshold expansion (9.12) and local increment estimate (9.13). The broader Section 8 globalization and all constant/profile extensions remain deliberately outside this PR.

[SamPetkov]

Follow-up organization: PR #31 now isolates the separate root-gap constant-propagation question. PR #30 remains limited to the Section 7 rate and Section 9 residual-restriction simplification; it does not depend on or assert the factor-four theorem constant.

[SamPetkov]

Review-sequence coordination is now documented in PR #33. The roadmap records this PR as the first recommended integration step and keeps its Section 7/9 simplifications logically separate from the constant work in #31 and #32.

[SamPetkov]

Follow-up: PR #34 translates this PR's direct matching-restriction subset-product argument into a focused Lean module. It proves the restriction injection, the ENNReal product bound, and its composition with the existing fixed-F aggregation. PR #34 remains draft until the warning-fatal Lean workflows complete.