Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Seam differences preserve signs

Abstract

Finite signed contraction on the actual rectangular height grid.

Definition 1.1 (The surviving-cell injection).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.cellExpand

Formalization. D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.cellExpand (✓ std3).

Citation. Chakshu Gupta (2026). One construction for the Miura-ori flip-graph degree sequence. DOI: 10.48550/arXiv.2607.05567. URL: https://arxiv.org/abs/2607.05567v3.

Commentary.

The map embeds the smaller physical rectangle in the original rectangle by skipping exactly the deleted internal column.

Theorem 1.2 (No surviving cells are identified).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.cellExpand_injective

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.cellExpand_injective (✓ std3). ∎

Citation. Chakshu Gupta (2026). One construction for the Miura-ori flip-graph degree sequence. DOI: 10.48550/arXiv.2607.05567. URL: https://arxiv.org/abs/2607.05567v3.

Commentary.

The surviving-cell map is injective on the actual rectangular cell type.

Theorem 1.3 (Every surviving cell is represented).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.cellExpand_surjOn

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.cellExpand_surjOn (✓ std3). ∎

Citation. Chakshu Gupta (2026). One construction for the Miura-ori flip-graph degree sequence. DOI: 10.48550/arXiv.2607.05567. URL: https://arxiv.org/abs/2607.05567v3.

Commentary.

Every original cell outside the deleted column is the image of one cell of the smaller rectangle.

Theorem 1.4 (The origin stays normalized).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.contractAt_isCanonicalHeight

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.contractAt_isCanonicalHeight (✓ std3). ∎

Citation. Chakshu Gupta (2026). One construction for the Miura-ori flip-graph degree sequence. DOI: 10.48550/arXiv.2607.05567. URL: https://arxiv.org/abs/2607.05567v3.

Commentary.

A normalized unit-edge height function remains normalized after signed deletion because the origin lies strictly before the removed internal column.

Theorem 1.5 (Seam differences preserve signs).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.contractAt_diff_seam_LtoR

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreCellExpand.contractAt_diff_seam_LtoR (✓ std3). ∎

Citation. Chakshu Gupta (2026). One construction for the Miura-ori flip-graph degree sequence. DOI: 10.48550/arXiv.2607.05567. URL: https://arxiv.org/abs/2607.05567v3.

Commentary.

Across the new seam the contracted height difference equals the corresponding original incident difference, using the uniform frozen slope.

References