Audit the full Erdős 625 proof stack and isolate reusable results - #39

Draft

SamPetkov wants to merge 76 commits into

agent/625-section8-all-deficit-amgmfrom

agent/625-full-proof-audit-frontier

Commits on Jul 24, 2026

Formalize matching-restriction product bound
SamPetkov
committed
e3bc89a
Add focused Lean check for matching restriction
SamPetkov
committed
90b83d1
Document matching-restriction formalization boundary
SamPetkov
committed
8605840

Commits on Jul 25, 2026

Fix focused Lean dependency build
SamPetkov
committed
35fa4f5
Add direct Section 9 attachment envelope
SamPetkov
committed
27c97b8
Document the direct attachment-envelope boundary
SamPetkov
committed
74b0df0
Add focused Lean gate for direct attachment envelope
SamPetkov
committed
957bba7
Expose focused Lean compiler tail
SamPetkov
committed
75bec86
Use targeted Lean dependency closure
SamPetkov
committed
4df65ce
Upload the focused Section 9 compiler log
SamPetkov
committed
425fe67
Repair the direct attachment-envelope transport
SamPetkov
committed
0c5c022
Use the exact ENNReal-to-EReal order bridge
SamPetkov
committed
3275046
State the direct endpoint in its native ENNReal codomain
SamPetkov
committed
0d627c2
Specialize the direct envelope to attained profile skeletons
SamPetkov
committed
1150060
Validate the attained-profile envelope endpoint
SamPetkov
committed
388c1ac
Extend the audit through the attained-profile bridge
SamPetkov
committed
d594979
Add the direct profile log-square adapter
SamPetkov
committed
64bde7c
Validate the direct log-square profile endpoint
SamPetkov
committed
b78e0ba
Record the direct log-square specialization
SamPetkov
committed
a3aa256
Cancel superseded focused envelope runs
SamPetkov
committed
fed5811
Silence the attained-profile cap linter
SamPetkov
committed
4a981d4
Fix the log-square imports and warning-fatal lints
SamPetkov
committed
628f0c2
Add q-only matching-restriction attachment envelope
SamPetkov
committed
1f11f8a
Add focused q-only attachment Lean workflow
SamPetkov
committed
f593ec2
Document q-only attachment envelope audit boundary
SamPetkov
committed
d0f95b5
Fix q-only pointwise domination proof
SamPetkov
committed
095288e
Add natural residual power dichotomy
SamPetkov
committed
b1d370f
Document the natural Section 9 power split
SamPetkov
committed
fb59f84
Specialize the q-only envelope to attained profiles
SamPetkov
committed
8808f03
Validate the attained-profile q-only endpoint
SamPetkov
committed
d7911a5
Fix q-only profile positivity and warning-fatal lint
SamPetkov
committed
892c413
Add the intrinsic profile residual dichotomy
SamPetkov
committed
6eb80a2
Validate the intrinsic profile residual split
SamPetkov
committed
55b9eb0
Expose the residual-mass abbreviation in the positivity proof
SamPetkov
committed
997d610
Normalize the intrinsic-split target before case analysis
SamPetkov
committed
ada3ea5
Cancel obsolete q-only validation runs
SamPetkov
committed
146a7bf
Fix warning-fatal q-only profile proof
SamPetkov
committed
f48c661
Fix warning-fatal intrinsic split proof
SamPetkov
committed
8c47f86
Assemble the q-only and small residual attachment regimes
SamPetkov
committed
2971838
Validate the q-only two-regime assembly
SamPetkov
committed
8333bc7
Avoid placeholder-word false positive in assembly documentation
SamPetkov
committed
2dd4279
Use an explicit positivity contradiction in the q-only profile adapter
SamPetkov
committed
33866e2
Use an explicit positivity contradiction in the intrinsic split
SamPetkov
committed
96f8e82
Repair the q-only two-regime filter and normalization bridges
SamPetkov
committed
7836b7d
Construct the q-only two-regime eventual bound explicitly
SamPetkov
committed
c7d2175
Fix Section 8 uniform product coercion proof
SamPetkov
committed
83c9466
Fix Section 8 all-high cell-weight normalization
SamPetkov
committed
e63a45f
Add full theorem-by-theorem Erdős 625 audit
SamPetkov
committed
e1bfca8
Add transferable Erdős 625 results and corollaries
SamPetkov
committed
c7689f0
Add exact regression checks for full proof audit
SamPetkov
committed
085cb66
Add focused CI for the full Erdős 625 audit
SamPetkov
committed
4468450
Repair q-only two-regime focused Lean target
SamPetkov
committed
d33b06d
Correct ENNReal namespace in q-only assembly
SamPetkov
committed
2ea82c9
Remove deprecated multiplication lemma from Section 8 product bound
SamPetkov
committed
6271bb8
Fix inverse-power normalization in Section 8 cell bound
SamPetkov
committed
bfc44f2
Use warning-free right multiplication monotonicity
SamPetkov
committed
f5471f6
Use the ENNReal inverse-power identity explicitly
SamPetkov
committed
95274c1
Integrate the verified Section 9 matching-restriction product
SamPetkov
committed
6459ede
Merge Section 9 simplification stack into the full 625 audit frontier
SamPetkov
authored
ce77809
Add the exact global Section 8 decoration bridge
SamPetkov
committed
20bc109
Extend the audit regression to the global Section 8 bridge
SamPetkov
committed
91a7fc2
Record the post-integration Erdős 625 proof frontier
SamPetkov
committed
4331369
Reduce the normalized second moment to the Section 8 bare sum
SamPetkov
committed
795f385
Check the exact q-only second-moment frontier in CI
SamPetkov
committed
cab2338
Commute the ENNReal product bound explicitly
SamPetkov
committed
e25005f
Correct the Section 8 bridge to an aggregate block-pairing comparison
SamPetkov
committed
4eeb9d6
Correct the post-integration Section 8 status
SamPetkov
committed
843d718
Extract the generic finite restriction-product theorem
SamPetkov
committed
ca23803
Keep the generic restriction-product theorem minimal
SamPetkov
committed
95a0838
Derive the matching product from the generic restriction theorem
SamPetkov
committed
396bc40
Document the generic restriction-product and forest generalization
SamPetkov
committed
afaa87b
Bridge subtype cardinality in the Section 8 decoration product
SamPetkov
committed
b0c2eaf
Make the all-high deficit cardinality type explicit
SamPetkov
committed
66e1e21
Repair the q-only second-moment frontier composition
SamPetkov
committed
b54d67e
Remove the deprecated multiplication monotonicity lemma
SamPetkov
committed
c651f0d
Normalize the matching-restriction focused Lean gate
SamPetkov
committed
ff70aa8