Documentation

LeanPool.CenteredMaximal.Lattice.Constants

The constants of the weighted lattice #

The chosen configuration is the periodic measure with columns at x = i * hgap, carrying mass 1 for even i and mass heavy for odd i, and rows at y = j * vgap of unit weight. Its parameters are determined by three edge collisions of witness rectangles; they reduce to the single quadratic 3 u² - 4 u - 6 = 0 for u = root = (2 + √22)/3:

heavy = u² - 1 = (17 + 4√22)/9, so a light and a heavy atom together weigh u²;
hgap = (1 + u)/2 = (5 + √22)/6 and vgap = hgap + 1 = (11 + √22)/6.

The witness squares use the sides 1, u, sideH1 = √heavy, sideLH2 = √2 · u, sideLHL2 = √(2 (2 + heavy)) and 2 hgap + 1. The witnesses cover the period cell outside four open slots, each of width slotW and height slotH, and phi = (2 hgap vgap - 4 slotW slotH) / (1 + heavy).

All numerical facts are proved from rational enclosures of √2 and √22.

noncomputable def LeanPool.CenteredMaximal.Lattice.root :

u = (2 + √22)/3, the positive root of 3u² - 4u - 6 = 0.

Equations

LeanPool.CenteredMaximal.Lattice.root = (2 + √22) / 3

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.heavy :

The heavy mass w = u² - 1 = (17 + 4√22)/9.

Equations

LeanPool.CenteredMaximal.Lattice.heavy = LeanPool.CenteredMaximal.Lattice.root ^ 2 - 1

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.hgap :

The column spacing h = (1 + u)/2 = (5 + √22)/6.

Equations

LeanPool.CenteredMaximal.Lattice.hgap = (1 + LeanPool.CenteredMaximal.Lattice.root) / 2

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.vgap :

The row spacing V = h + 1 = (11 + √22)/6.

Equations

LeanPool.CenteredMaximal.Lattice.vgap = LeanPool.CenteredMaximal.Lattice.hgap + 1

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.sideH1 :

Side of the witness made of one heavy atom: √w.

Equations

LeanPool.CenteredMaximal.Lattice.sideH1 = √LeanPool.CenteredMaximal.Lattice.heavy

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.sideLH2 :

Side of the witness made of a light and a heavy atom in two rows: √(2(1 + w)) = √2 · u.

Equations

LeanPool.CenteredMaximal.Lattice.sideLH2 = √2 * LeanPool.CenteredMaximal.Lattice.root

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.sideLHL2 :

Side of the witness made of light, heavy, light atoms in two rows: √(2(2 + w)).

Equations

LeanPool.CenteredMaximal.Lattice.sideLHL2 = √(2 * (2 + LeanPool.CenteredMaximal.Lattice.heavy))

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.slotW :

Width of a slot excluded from the witnessed region: 2h - √(2(2 + w))/2 - u/2.

Equations

LeanPool.CenteredMaximal.Lattice.slotW = 2 * LeanPool.CenteredMaximal.Lattice.hgap - LeanPool.CenteredMaximal.Lattice.sideLHL2 / 2 - LeanPool.CenteredMaximal.Lattice.root / 2

Instances For

noncomputable def LeanPool.CenteredMaximal.Lattice.slotH :

Height of a slot excluded from the witnessed region: V - √(2(1 + w))/2 - √w/2.

Equations

LeanPool.CenteredMaximal.Lattice.slotH = LeanPool.CenteredMaximal.Lattice.vgap - LeanPool.CenteredMaximal.Lattice.sideLH2 / 2 - LeanPool.CenteredMaximal.Lattice.sideH1 / 2

Instances For

Square roots #

theorem LeanPool.CenteredMaximal.Lattice.sqrt22_sq :

√22 ^ 2 = 22

theorem LeanPool.CenteredMaximal.Lattice.sqrt22_gt :

4.69 < √22

Lower rational enclosure of √22.

theorem LeanPool.CenteredMaximal.Lattice.sqrt22_lt :

√22 < 4.691

Upper rational enclosure of √22.

theorem LeanPool.CenteredMaximal.Lattice.sqrt2_gt :

1.414 < √2

Lower rational enclosure of √2.

theorem LeanPool.CenteredMaximal.Lattice.sqrt2_lt :

√2 < 1.4143

Upper rational enclosure of √2.

Exact identities #

theorem LeanPool.CenteredMaximal.Lattice.root_quadratic :

3 * root ^ 2 - 4 * root - 6 = 0

3u² - 4u - 6 = 0.

theorem LeanPool.CenteredMaximal.Lattice.two_mul_hgap_sub_one :

2 * hgap - 1 = root

u = 2h - 1: the light–heavy one-row witness starts where the light atom's square ends.

theorem LeanPool.CenteredMaximal.Lattice.one_add_heavy :

1 + heavy = root ^ 2

A light and a heavy atom together weigh u².

theorem LeanPool.CenteredMaximal.Lattice.vgap_eq :

vgap = hgap + 1

V = h + 1.

theorem LeanPool.CenteredMaximal.Lattice.heavy_eq :

heavy = (17 + 4 * √22) / 9

w = (17 + 4√22)/9.

theorem LeanPool.CenteredMaximal.Lattice.two_mul_hgap_add_one_sq :

(2 * hgap + 1) ^ 2 = 2 * (heavy + 1 + heavy)

The side 2h + 1 of the heavy–light–heavy two-row witness squares to its mass.

Numerical facts #

theorem LeanPool.CenteredMaximal.Lattice.root_gt :

2.23 < root

theorem LeanPool.CenteredMaximal.Lattice.root_lt :

root < 2.2304

Upper enclosure of u.

theorem LeanPool.CenteredMaximal.Lattice.one_le_root :

1 ≤ u, so the light–heavy one-row witness has side at least 1.

theorem LeanPool.CenteredMaximal.Lattice.heavy_gt :

3.9729 < heavy

Lower enclosure of w.

theorem LeanPool.CenteredMaximal.Lattice.heavy_lt :

heavy < 3.9747

Upper enclosure of w.

theorem LeanPool.CenteredMaximal.Lattice.heavy_pos :

The heavy mass is positive.

theorem LeanPool.CenteredMaximal.Lattice.hgap_gt :

1.615 < hgap

Lower enclosure of h.

theorem LeanPool.CenteredMaximal.Lattice.hgap_lt :

hgap < 1.6152

Upper enclosure of h.

theorem LeanPool.CenteredMaximal.Lattice.hgap_pos :

The column spacing is positive.

theorem LeanPool.CenteredMaximal.Lattice.vgap_gt :

2.615 < vgap

Lower enclosure of V.

theorem LeanPool.CenteredMaximal.Lattice.vgap_lt :

vgap < 2.6152

Upper enclosure of V.

theorem LeanPool.CenteredMaximal.Lattice.sideLH2_sq :

sideLH2 ^ 2 = 2 * (1 + heavy)

The light–heavy two-row witness squares to its mass 2(1 + w).

theorem LeanPool.CenteredMaximal.Lattice.sideH1_sq :

sideH1 ^ 2 = heavy

The one-heavy-atom witness squares to its mass w.

theorem LeanPool.CenteredMaximal.Lattice.sideLHL2_sq :

sideLHL2 ^ 2 = 2 * (1 + heavy + 1)

The light–heavy–light two-row witness squares to its mass 2(2 + w).

theorem LeanPool.CenteredMaximal.Lattice.sideLH2_gt :

3.153 < sideLH2

Lower enclosure of √2 u.

theorem LeanPool.CenteredMaximal.Lattice.sideLH2_lt :

sideLH2 < 3.1545

Upper enclosure of √2 u.

theorem LeanPool.CenteredMaximal.Lattice.sideH1_gt :

Lower enclosure of √w.

theorem LeanPool.CenteredMaximal.Lattice.sideH1_lt :

sideH1 < 1.994

Upper enclosure of √w.

theorem LeanPool.CenteredMaximal.Lattice.sideLHL2_gt :

3.45 < sideLHL2

Lower enclosure of √(2(2 + w)).

theorem LeanPool.CenteredMaximal.Lattice.sideLHL2_lt :

sideLHL2 < 3.457

Upper enclosure of √(2(2 + w)).

theorem LeanPool.CenteredMaximal.Lattice.one_le_sideH1 :

1 ≤ √w: the heavy atom's square reaches back to the light–heavy one-row region.

theorem LeanPool.CenteredMaximal.Lattice.root_le_sideLH2 :

root ≤ sideLH2

u ≤ √2 u: the light–heavy two-row witness is wider than the one-row one.

theorem LeanPool.CenteredMaximal.Lattice.vgap_le_sideLH2 :

vgap ≤ sideLH2

V ≤ √2 u: the light–heavy two-row witness reaches the middle line y = V/2.

theorem LeanPool.CenteredMaximal.Lattice.two_mul_vgap_le_root_add_sideLH2 :

2 * vgap ≤ root + sideLH2

2V ≤ u + √2 u: above the one-row witness the two-row witness takes over.

theorem LeanPool.CenteredMaximal.Lattice.two_mul_hgap_le_sideLHL2 :

2 * hgap ≤ sideLHL2

2h ≤ √(2(2 + w)): the light–heavy–light witness reaches the heavy column.

theorem LeanPool.CenteredMaximal.Lattice.vgap_le_sideLHL2 :

vgap ≤ sideLHL2

V ≤ √(2(2 + w)): the light–heavy–light witness reaches the middle line y = V/2.

theorem LeanPool.CenteredMaximal.Lattice.vgap_sub_le_sideH1 :

2 * vgap - sideLHL2 ≤ sideH1

2V - √(2(2 + w)) ≤ √w: next to the heavy column the two witnesses overlap.

theorem LeanPool.CenteredMaximal.Lattice.four_mul_hgap_sub_le_sideLH2 :

4 * hgap - sideLHL2 ≤ sideLH2

4h - √(2(2 + w)) ≤ √2 u: left of the heavy column the two-row witnesses overlap.

theorem LeanPool.CenteredMaximal.Lattice.slotW_pos :

The slot has positive width.

theorem LeanPool.CenteredMaximal.Lattice.slotH_pos :

The slot has positive height.

The closed form of `Φ` #

theorem LeanPool.CenteredMaximal.Lattice.sqrt2_mul_sqrt22 :

√2 * √22 = 2 * √11

theorem LeanPool.CenteredMaximal.Lattice.sqrt_div_nine {x : ℝ} (hx : 0 ≤ x) :

√(x / 9) = √x / 3

√(x/9) = √x / 3.

theorem LeanPool.CenteredMaximal.Lattice.sideLH2_eq :

sideLH2 = (2 * √2 + 2 * √11) / 3

√2 u = (2√2 + 2√11)/3.

theorem LeanPool.CenteredMaximal.Lattice.sideH1_eq :

sideH1 = √(17 + 4 * √22) / 3

√w = √(17 + 4√22)/3.

theorem LeanPool.CenteredMaximal.Lattice.sideLHL2_eq :

sideLHL2 = √(70 + 8 * √22) / 3

√(2(2 + w)) = √(70 + 8√22)/3.

theorem LeanPool.CenteredMaximal.Lattice.slotW_eq :

slotW = (8 + √22 - √(70 + 8 * √22)) / 6

The slot width in radicals.

theorem LeanPool.CenteredMaximal.Lattice.slotH_eq :

slotH = (11 + √22 - 2 * √2 - 2 * √11 - √(17 + 4 * √22)) / 6

The slot height in radicals.

theorem LeanPool.CenteredMaximal.Lattice.one_add_heavy_eq :

1 + heavy = (26 + 4 * √22) / 9

The mass per period cell in radicals.

theorem LeanPool.CenteredMaximal.Lattice.two_mul_hgap_mul_vgap :

2 * hgap * vgap = (77 + 16 * √22) / 18

The area of the period cell in radicals.

theorem LeanPool.CenteredMaximal.Lattice.phi_eq :

phi = (2 * hgap * vgap - 4 * slotW * slotH) / (1 + heavy)

The expression for Φ used in the area lower bound: subtract the four slot areas slotW · slotH from the cell area 2 h V, then divide by the cell mass 1 + w.