Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Both boundary columns are occupied

Abstract

Finite signed contraction on the actual rectangular height grid.

Theorem 1.1 (A boundary walk has an extremum).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.boundary_walk_abstract

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.boundary_walk_abstract (✓ 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.

Two compatible unit-step integer walks joined by unit horizontal differences have a row with all existing neighbours uniformly higher or uniformly lower.

Theorem 1.2 (The first column is occupied).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.firstColumn_active

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.firstColumn_active (✓ 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.

In a unit-edge height function with nonempty rows and at least two columns, the first physical column contains an ambient strict extremum.

Theorem 1.3 (The last column is occupied).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.lastColumn_active

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.lastColumn_active (✓ 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 last physical column also contains an ambient strict extremum, with all existing vertical and horizontal neighbours included.

Theorem 1.4 (Both boundary columns are occupied).

Lean statement: D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.boundary_columns_active

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Geometry/MiuraCoreBoundary.boundary_columns_active (✓ 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 first and last physical columns are simultaneously occupied in the same height function.

References