Non-vacuity witnesses for indexed word realizations #

Explicit real configurations inhabit each of the thirteen exceptional-word realization predicates routed through the four shared closure families.

Non-vacuity witnesses for the exceptional-word realizations #

source

def LeanPool.Erdos132ConvexK3.Witnesses.terminalWordPoints :

Fin 5 → Point ℝ

A rational terminal-cage pentagon in the intended cyclic order x, vertex, t, w, s.

Equations

LeanPool.Erdos132ConvexK3.Witnesses.terminalWordPoints i = match ↑i with | 0 => (0, 0) | 1 => (725, -29) | 2 => (2900, 0) | 3 => (1425, 2600) | x => (725, 2900)

Instances For

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row1_B32_realization_nonempty :

WordRealization ExceptionalCoverWord.row1_B32 terminalWordPoints 13140625 8935625 8790625

The terminal pentagon inhabits the row-1 B:3→2 realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row4_D32_realization_nonempty :

WordRealization ExceptionalCoverWord.row4_D32 terminalWordPoints 13140625 8935625 8790625

The terminal pentagon also inhabits the reflected row-4 D:3→2 tag.

source

def LeanPool.Erdos132ConvexK3.Witnesses.sharedTipPoints :

Fin 6 → Point ℝ

An integer-scaled rational shared-tip configuration in cyclic order e, vertex, t, w, s, r.

Equations

LeanPool.Erdos132ConvexK3.Witnesses.sharedTipPoints i = match ↑i with | 0 => (0, 0) | 1 => (559, -13) | 2 => (1300, 0) | 3 => (790, 1220) | 4 => (650, 1300) | x => (510, 1220)

Instances For

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row1_B31_realization_nonempty :

WordRealization ExceptionalCoverWord.row1_B31 sharedTipPoints 2112500 1748500 1732250

The shared-tip hexagon inhabits the row-1 B:3→1 realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row2_BA_realization_nonempty :

WordRealization ExceptionalCoverWord.row2_BA sharedTipPoints 2112500 1748500 1732250

The shared-tip hexagon inhabits the row-2 BA realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row4_D31_realization_nonempty :

WordRealization ExceptionalCoverWord.row4_D31 sharedTipPoints 2112500 1748500 1732250

The shared-tip hexagon inhabits the row-4 D:3→1 realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row4_DC_realization_nonempty :

WordRealization ExceptionalCoverWord.row4_DC sharedTipPoints 2112500 1748500 1732250

The shared-tip hexagon inhabits the row-4 DC realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row1_B21_realization_nonempty :

WordRealization ExceptionalCoverWord.row1_B21 sharedTipPoints 2112500 1748500 1732250

The two-rung hexagon inhabits the row-1 B:2→1 realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row2_AB_realization_nonempty :

WordRealization ExceptionalCoverWord.row2_AB sharedTipPoints 2112500 1748500 1732250

The two-rung hexagon inhabits the row-2 AB realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row3_BB_DD_realization_nonempty :

WordRealization ExceptionalCoverWord.row3_BB_DD sharedTipPoints 2112500 1748500 1732250

The two-rung hexagon inhabits the row-3 BB×DD realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row4_D21_realization_nonempty :

WordRealization ExceptionalCoverWord.row4_D21 sharedTipPoints 2112500 1748500 1732250

The two-rung hexagon inhabits the row-4 D:2→1 realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row4_CD_realization_nonempty :

WordRealization ExceptionalCoverWord.row4_CD sharedTipPoints 2112500 1748500 1732250

The two-rung hexagon inhabits the row-4 CD realization.

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row5_BB_DD_realization_nonempty :

WordRealization ExceptionalCoverWord.row5_BB_DD sharedTipPoints 2112500 1748500 1732250

The two-rung hexagon inhabits the row-5 BB×DD realization.

source

def LeanPool.Erdos132ConvexK3.Witnesses.fourEdgePoints :

Fin 6 → Point ℝ

A rational six-point four-edge cage with two distinct lower endpoints.

Equations

LeanPool.Erdos132ConvexK3.Witnesses.fourEdgePoints i = match ↑i with | 0 => (0, 0) | 1 => (559, -13) | 2 => (741, -13) | 3 => (1300, 0) | 4 => (790, 1220) | x => (510, 1220)

Instances For

source

theorem LeanPool.Erdos132ConvexK3.Witnesses.row4_DD_realization_nonempty :

WordRealization ExceptionalCoverWord.row4_DD fourEdgePoints 2112500 1748500 1690000

The explicit four-edge cage inhabits the row-4 DD realization.