Integrate the direct Section 9 attachment and log-square envelope

[SamPetkov]

Summary

This is a stacked follow-up to PR #34. Its base is agent/625-lean-matching-restriction-product, so the diff isolates the analytic, actual-attachment, attained-profile, and asymptotic integration built on the finite matching-restriction product theorem.

The final target on this branch is the uniform large-residual endpoint

profileHighSkeletonAttachment
  <= exp(C * (log n)^2).

It contains no cycle-traversal parameter, no profile-block-cardinality term, and no matching-cardinality term.

Files

• 625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
• 625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
• 625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
• 625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
• .github/workflows/erdos625-matching-restriction-envelope.yml

Finite theorem chain

1. sum_configurationCellTheta_sq_global proves

   sum theta_ab^2
     = (e/m)^2 * (sum row_a^2) * (sum col_b^2).
   

2. sum_configurationCellTheta_sq_le_euler_sq_cap_sq applies equal positive totals and degree caps:

   sum theta_ab^2 <= e^2 * U^2.
   

3. existsAbsoluteResidualQTotalBound_of_degreeCaps sums the accepted pointwise quadratic residualQ estimate:

   sum q_ab <= kappaQ * U^2.
   

4. residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct combines PR Kernel-check the Section 9 matching-restriction product bound #34 with the exact fixed-family Fubini identity, so the direct product applies to the literal cap/no-return attachment numerator.

5. lambda_matching_products_le_exp_of_sum_bounds converts the lambda and outside-matching products to one exponential.

6. exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope obtains

   residualActualAttachmentNumerator
     <= exp(kappaLambda * U^4/m + kappaQ * U^2).
   

Attained-profile and asymptotic specialization

exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope transports the finite result to every attained profile high skeleton through its canonical reference witness and literal residual degree lists.

matchingRestrictionEnvelope_bound proves the exact real estimate

kappaLambda * U^4/m + kappaQ * U^2
  <= (kappaLambda * C_U^4 + kappaQ * C_U^2) * L^2

under m >= n/L^6, U <= C_U L, and L^8 <= n.

Finally, eventually_profileHighSkeletonAttachment_le_matching_logScale specializes L=log n and the phase cap to give the uniform exp(O((log n)^2)) endpoint.

Improvement over the existing route

The current formal large-residual endpoint uses residual-only and mixed-cycle walk enumeration and produces a coarse exponent containing profile-block and matching-support terms. The direct restriction route removes those terms and kernel-checks the manuscript simplification proposed in PR #30.

The older traversal development remains untouched and independently useful.

Validation

The focused workflow rejects placeholders and project-defined axioms, prepares the pinned Lean 4.31/mathlib project, and builds the log-square profile endpoint with its dependency closure under --wfail. The full repository Lean workflow also runs.

The focused workflow uploads the exact compiler log on every run; prior failed iterations exposed only theorem-transport/coercion issues and were patched without weakening the statements.

Scope boundary

This PR does not yet:

• integrate the modules into Erdos625.lean, the axiom audit, or the generated self-contained checkpoint;
• prove the Section VIII bare-skeleton sum;
• combine this direct large-residual endpoint with the existing small-residual endpoint in one new profile two-regime theorem;
• prove Proposition 9.2, the chromatic lower tail, the final event intersection, or Erdos625Statement.

PR #34 should be merged first; this PR can then be retargeted to main.

[SamPetkov]

Follow-up simplification: PR #37 absorbs the local residualLambda product into the same total residualQ mass, yielding a q-only exp(O(U^2)) attachment envelope. It also packages the two residual regimes through the intrinsic finite split 2^U <= m^3 versus m < 2^ceil(U/3). PR #35 should remain the reviewed literal-attachment integration layer; #37 is stacked on top of it.