Skip to content

Family-130 arbitrary-prefix side-row certificate

Choose a tag to compare

View all tags
@whyihaveyou whyihaveyou released this 07 Oct 07:20
· 294 commits to scope-130-parameter-certificate since this release
v0.2.2-arbitrary-side-row
b18e10d

This release generalizes the side-row frame certificate to arbitrary finite prefix types.

  • SideRowGeneralArbitrary.lean uses the generic contraction/insertion maps from CenterRowGeneral.lean for E = ι × Fin h → F₂, with arbitrary finite ι.
  • It proves the exact side-row decomposition L5 = L2 ⊔ residual, disjointness of the old row and inserted pair complement, surjectivity/kernel formulas for the two-label map, and residual finrank h - 2.

The module builds under the repository's autoImplicit=false configuration with no sorry or newly introduced axioms. It is a reusable local frame interface, not a completed eight-row schedule or an all-length DFT theorem.

Assets 2
Loading