Integrate the verified Section 9 stack into the full 625 audit frontier - #40

Merged

SamPetkov merged 47 commits into

agent/625-full-proof-audit-frontierfrom

agent/625-q-only-attachment-envelope

Jul 25, 2026

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
Repair q-only two-regime focused Lean target
SamPetkov
committed
d33b06d
Correct ENNReal namespace in q-only assembly
SamPetkov
committed
2ea82c9