Close the Section 8 physical-fibre and all-deficit seam - #45

Draft

SamPetkov wants to merge 26 commits into

agent/625-full-tex-mathematical-reauditfrom

agent/625-section8-physical-fibre-closure

Commits on Jul 26, 2026

Add focused CI for the Section 8 physical-fibre closure
SamPetkov
committed
c201d2c
Validate the physical endpoint block-pairing reconstruction
SamPetkov
committed
5107924
Gate the validated block-reverse checkpoint independently
SamPetkov
committed
73e25c3
Add the exact partial-cell physical fibre and aggregate weight
SamPetkov
committed
2579909
Discharge the endpoint slot coercions explicitly
SamPetkov
committed
1864198
Unfold the local block-pair abbreviation in the reverse map
SamPetkov
committed
bcbf1ef
Reconstruct local endpoint stub matchings from a physical fibre
SamPetkov
committed
320b3f3
Build every accepted Section 8 closure checkpoint
SamPetkov
committed
d67206f
Add exact regression checks for the physical-fibre closure
SamPetkov
committed
c365b52
Run exact closure regression beside the Lean checkpoints
SamPetkov
committed
f57cad1
Make the independent deficit-function binders anonymous
SamPetkov
committed
3341074
Prove the endpoint decorated/physical equivalence
SamPetkov
committed
bcfa19f
Resolve the endpoint round trips by block substitution
SamPetkov
committed
0e3bd11
Extract the block support and all-high deficits of an attained demand
SamPetkov
committed
02ed1a3
Expose the numerical value preserved by the endpoint stub cast
SamPetkov
committed
d47f954
Repair the endpoint physical round-trip equalities
SamPetkov
committed
62bc992
Add the attained-demand support checkpoint to focused CI
SamPetkov
committed
51924ad
Eliminate dependent Sigma and substitution failures in the endpoint equivalence
SamPetkov
committed
06eab2a
Make the endpoint reverse edge equality explicit
SamPetkov
committed
ec7b730
Use Fin heterogeneous extensionality in the endpoint inverse
SamPetkov
committed
2ce7afe
Pass natural bound equalities to Fin heterogeneous extensionality
SamPetkov
committed
ad52e5e
Rewrite shared endpoints before applying support matchingness
SamPetkov
committed
ce4c683
Derive the endpoint block cover from four-deficit support
SamPetkov
committed
6ce121d
Build the four-deficit endpoint-cover adapter in focused CI
SamPetkov
committed
20a7238
Split the four-support alternatives explicitly
SamPetkov
committed
5ca2856
Recover the endpoint coordinate from its real deficit
SamPetkov
committed
e5752da

Navigation Menu

Close the Section 8 physical-fibre and all-deficit seam - #45

Close the Section 8 physical-fibre and all-deficit seam#45
SamPetkov wants to merge 26 commits into
agent/625-full-tex-mathematical-reauditfrom
agent/625-section8-physical-fibre-closure

Commits on Jul 26, 2026

Add focused CI for the Section 8 physical-fibre closure

Validate the physical endpoint block-pairing reconstruction

Gate the validated block-reverse checkpoint independently

Add the exact partial-cell physical fibre and aggregate weight

Discharge the endpoint slot coercions explicitly

Unfold the local block-pair abbreviation in the reverse map

Reconstruct local endpoint stub matchings from a physical fibre

Build every accepted Section 8 closure checkpoint

Add exact regression checks for the physical-fibre closure

Run exact closure regression beside the Lean checkpoints

Make the independent deficit-function binders anonymous

Prove the endpoint decorated/physical equivalence

Resolve the endpoint round trips by block substitution

Extract the block support and all-high deficits of an attained demand

Expose the numerical value preserved by the endpoint stub cast

Repair the endpoint physical round-trip equalities

Add the attained-demand support checkpoint to focused CI

Eliminate dependent Sigma and substitution failures in the endpoint equivalence

Make the endpoint reverse edge equality explicit

Use Fin heterogeneous extensionality in the endpoint inverse

Pass natural bound equalities to Fin heterogeneous extensionality

Rewrite shared endpoints before applying support matchingness

Derive the endpoint block cover from four-deficit support

Build the four-deficit endpoint-cover adapter in focused CI

Split the four-support alternatives explicitly

Recover the endpoint coordinate from its real deficit