Charging

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

noncomputable def ConwaySoifer.Simplified.penalty (T : Configuration) (r : ℝ) (i : Fin 6) : ℝ

A corner cap is paid by a side owner with loss at least r²/4.

Equations

• ConwaySoifer.Simplified.penalty T r i = if r ^ 2 / 4 ≤ ConwaySoifer.sideLoss T i then r ^ 2 / 23 else 0

theorem ConwaySoifer.Simplified.cornerHelp_le_charges {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (charge : Fin 6 → ℝ) (hnonneg : ∀ (i : Fin 6), 0 ≤ charge i) (hpay : ∀ (j : Fin 3) (m : Fin 2) (i : Fin 6), cornerMid j m ∈ (T (sideIndex i)).carrier → r ^ 2 / 23 ≤ charge i) : ∑ j : Fin 3, ⋯.toAnchored.cornerHelp j ≤ ∑ i : Fin 6, charge i

Abstract charging: each corner chooses a missing midpoint; locality assigns it to one of that corner's two side owners. Summing counts each side once.

theorem ConwaySoifer.Simplified.charged_budget {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) : ∑ i : Fin 6, (sideLoss T i - penalty T r i) ≤ 7 * r ^ 2 - 6

theorem ConwaySoifer.Simplified.section_sq_lt {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) : s ^ 2 < 13 * r ^ 2 / 69

theorem ConwaySoifer.Simplified.effective_loss_ge {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (i : Fin 6) : s ^ 2 ≤ sideLoss T i - penalty T r i

theorem ConwaySoifer.Simplified.penalty_le {T : Configuration} {r : ℝ} (i : Fin 6) : penalty T r i ≤ r ^ 2 / 23

theorem ConwaySoifer.Simplified.sint_upper {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sint T r s) : s < 9 / 25

The strengthened upper endpoint for internal transfer.

theorem ConwaySoifer.Simplified.small_side_no_cost {c : ContactCase} {T : Configuration} {r s : ℝ} (H : Canonical c T r s) (hS : c.isS) (hs : s ≤ 1 / 10) (i : Fin 6) (hi : i ≠ recvOf c) : sideLoss T i < r ^ 2 / 4

In the small side cases no nonreceiver can have midpoint-sized loss.

theorem ConwaySoifer.Simplified.sext_receiver_no_mid {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) (j : Fin 3) (m : Fin 2) : cornerMid j m ∉ (T (sideIndex 5)).carrier

The external receiver cannot pay for any corner midpoint.

noncomputable def ConwaySoifer.Simplified.sextPenalty (T : Configuration) (r : ℝ) (i : Fin 6) : ℝ

The side-owner penalty with the Sext receiver's contribution set to zero.

Equations

• ConwaySoifer.Simplified.sextPenalty T r i = if i = 5 then 0 else ConwaySoifer.Simplified.penalty T r i

theorem ConwaySoifer.Simplified.sext_charged_budget {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) : ∑ i : Fin 6, (sideLoss T i - sextPenalty T r i) ≤ 7 * r ^ 2 - 6

theorem ConwaySoifer.Simplified.sext_effective_ge {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) (i : Fin 6) : s ^ 2 ≤ sideLoss T i - sextPenalty T r i

theorem ConwaySoifer.Simplified.sext_no_cost {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) (i : Fin 6) (hi : i ≠ 5) : sideLoss T i < r ^ 2 / 4

theorem ConwaySoifer.Simplified.sext_upper {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) : s < 1 / 3

External transfer is impossible at and above 1/3.