Integrate the direct Section 9 attachment and log-square envelope - #35

Open

SamPetkov wants to merge 18 commits into

agent/625-lean-matching-restriction-productfrom

agent/625-section9-direct-attachment-envelope

Commits on Jul 25, 2026

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