Absorb Section 9 into a q-only intrinsic residual split

[SamPetkov]

Summary

This is a stacked follow-up to PR #35. It removes the redundant analytic split in the direct matching-restriction attachment route, carries the simplification through the attained-profile layer, and packages both residual regimes into a literal attachment-sum estimate.

Outside the exposed matching,

residualQ = theta^2 / 2 + residualLambda,

so residualLambda <= residualQ pointwise. The same total-q bound controls both the local-increment product and the direct outside-matching q product.

Main q-only conclusion

For one absolute positive finite constant kappa,

residualActualAttachmentNumerator
  <= exp(kappa * U^2)

under the degree caps and exact quadratic condition 2^U <= m^3.

This replaces

kappaLambda * U^4/m + kappaQ * U^2

by a single O(U^2) term. The final route no longer needs the separate total-lambda estimate or its cubic degree-moment calculation.

Files

• 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
• 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
• 625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
• 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
• 625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
• .github/workflows/erdos625-q-only-attachment-envelope.yml

Theorem chain

1. residualLambda_le_residualQ proves pointwise domination.
2. lambda_matching_products_le_exp_two_q_bound charges both finite products to twice one total-q sum.
3. exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope combines this with the accepted total-q estimate at scale U^2.
4. exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope specializes the finite result to every attained canonical high skeleton.
5. eventually_profileHighSkeletonAttachment_le_qOnly_logScale gives the uniform profile endpoint exp(O((log n)^2)) in the quadratic regime.
6. exists_absolute_profileHighSkeletonAttachment_intrinsic_split packages the quadratic and deterministic branches in one exact finite statement.
7. exists_midpointCanonicalAttachment_qOnly_twoRegime_error combines the two regimes over the literal attained attachment sum and produces a deterministic coefficient epsilon_n -> 0 at scale n/(log n)^4.

Finite regime split and phase assembly

The module proves

not (2^U <= m^3)  ->  m < 2^ceil(U/3),
ceil(U/3) = (U+2)/3.

The profile-level split is therefore:

• 2^U <= m^3: attachment <= exp(kappa U^2);
• 2^U > m^3: m < 2^ceil(U/3) and attachment <= 2^(U m/2).

The exported assembly theorem uses the phase-controlled implication in the large-residual range and the literal deterministic bound in the complementary range. It concludes

midpointCanonicalAttachmentSum
  <= canonicalBareSkeletonSum * exp(epsilon_n * n/log(n)^4),
epsilon_n -> 0.

Thus Section IX is reduced to the Section VIII bare-skeleton estimate; no independent polymer surrogate or remaining Section IX phase adapter is needed.

Validation

The focused workflow rejects placeholders and project-defined axioms/constants and builds the q-only two-regime assembly with its dependency closure under Lean 4.31 and --wfail.

The focused run succeeded at commit 2ea82c988218dee89d3639f598090ce813501c40. The repaired proof replaces three brittle automation steps by explicit Nat.max monotonicity and removes a redundant algebra tactic after field_simp.

This branch was mechanically integrated into the cumulative audit head through PR #40; PR #39 now contains both the Section VIII and Section IX simplification lines.

Scope boundary

This PR does not bound the Section VIII bare skeleton sum, prove the final normalized second-moment estimate without that Section VIII input, rewrite the canonical manuscript, or prove Erdos625Statement.

PR #34 and PR #35 should still be reviewed first in the original stack. The cumulative cross-stack review is PR #39.