Moving sofa: related mathematical developments

• Gerver.Foundations.Development001.

Moving sofa: related mathematical developments

• Gerver.AreaCertificate.
• Gerver.Area.TrigEnclosure.

Exact rational certificate for the Gerver cap and niche areas

This module carries the finite, kernel-checkable part of the rational area bounds for Gerver's sofa: integer interval arithmetic at scale M = 10 ^ 30, certified enclosures of the twenty-two direct parameters and of π, interval sine and cosine by the Taylor recurrence, the grid of rotation angles, the five phase formulas, the support-contact fan of the cap and the rectangle cover of the niche.

Everything here is computable and decide +kernel-checkable; the two closed numeric conclusions capOK_true and nicheOK_true are the only facts the analytic layer in MovingSofa.Gerver.Area needs from this module.

Integer interval arithmetic at scale 10 ^ 30

The kernel accelerates Int arithmetic but not Rat arithmetic, so the whole finite calculation is carried out on pairs of integers denoting the interval [lo / M, hi / M].

def MovingSofa.GerverAreaCert.M : ℤ

The common denominator of every interval endpoint.

Equations

• MovingSofa.GerverAreaCert.M = 10 ^ 30

structure MovingSofa.GerverAreaCert.SI : Type

⟨lo, hi⟩ denotes the real interval [lo / M, hi / M].

• lo : ℤ

  The scaled integer lower endpoint.

• hi : ℤ

  The scaled integer upper endpoint.

def MovingSofa.GerverAreaCert.instDecidableEqSI.decEq (x✝ x✝¹ : SI) : Decidable (x✝ = x✝¹)

Equations

• MovingSofa.GerverAreaCert.instDecidableEqSI.decEq { lo := a, hi := a_1 } { lo := b, hi := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance MovingSofa.GerverAreaCert.instDecidableEqSI : DecidableEq SI

Equations

• MovingSofa.GerverAreaCert.instDecidableEqSI = MovingSofa.GerverAreaCert.instDecidableEqSI.decEq

def MovingSofa.GerverAreaCert.SI.imin (a b : ℤ) : ℤ

Kernel-cheap min on ℤ.

Equations

• MovingSofa.GerverAreaCert.SI.imin a b = if a ≤ b then a else b

def MovingSofa.GerverAreaCert.SI.imax (a b : ℤ) : ℤ

Kernel-cheap max on ℤ.

Equations

• MovingSofa.GerverAreaCert.SI.imax a b = if a ≤ b then b else a

def MovingSofa.GerverAreaCert.SI.ratI (a b : ℤ) : SI

Outward enclosure of a / b for 0 < b.

Equations

• MovingSofa.GerverAreaCert.SI.ratI a b = { lo := a * MovingSofa.GerverAreaCert.M / b, hi := -(-(a * MovingSofa.GerverAreaCert.M) / b) }

def MovingSofa.GerverAreaCert.SI.zero : SI

The exact interval [0, 0].

Equations

• MovingSofa.GerverAreaCert.SI.zero = { lo := 0, hi := 0 }

def MovingSofa.GerverAreaCert.SI.one : SI

The exact interval [1, 1].

Equations

• MovingSofa.GerverAreaCert.SI.one = { lo := MovingSofa.GerverAreaCert.M, hi := MovingSofa.GerverAreaCert.M }

def MovingSofa.GerverAreaCert.SI.add (x y : SI) : SI

Interval addition.

Equations

• x.add y = { lo := x.lo + y.lo, hi := x.hi + y.hi }

def MovingSofa.GerverAreaCert.SI.neg (x : SI) : SI

Interval negation.

Equations

• x.neg = { lo := -x.hi, hi := -x.lo }

def MovingSofa.GerverAreaCert.SI.sub (x y : SI) : SI

Interval subtraction.

Equations

• x.sub y = { lo := x.lo - y.hi, hi := x.hi - y.lo }

def MovingSofa.GerverAreaCert.SI.mul (x y : SI) : SI

Interval multiplication: the extreme endpoint products, rounded outward.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.SI.divn (x : SI) (b : ℤ) : SI

Division by a positive integer.

Equations

• x.divn b = { lo := x.lo / b, hi := -(-x.hi / b) }

def MovingSofa.GerverAreaCert.SI.imul (k : ℤ) (x : SI) : SI

Multiplication by an integer.

Equations

• MovingSofa.GerverAreaCert.SI.imul k x = { lo := MovingSofa.GerverAreaCert.SI.imin (k * x.lo) (k * x.hi), hi := MovingSofa.GerverAreaCert.SI.imax (k * x.lo) (k * x.hi) }

Real semantics and soundness

def MovingSofa.GerverAreaCert.SI.Contains (z : SI) (x : ℝ) : Prop

z denotes the real interval [z.lo / M, z.hi / M].

Equations

• z.Contains x = (↑z.lo ≤ ↑MovingSofa.GerverAreaCert.M * x ∧ ↑MovingSofa.GerverAreaCert.M * x ≤ ↑z.hi)

theorem MovingSofa.GerverAreaCert.SI.imin_eq_min (a b : ℤ) : imin a b = min a b

imin is min.

theorem MovingSofa.GerverAreaCert.SI.imax_eq_max (a b : ℤ) : imax a b = max a b

imax is max.

theorem MovingSofa.GerverAreaCert.SI.Mpos : 0 < ↑M

The scale is positive.

theorem MovingSofa.GerverAreaCert.SI.ediv_le_of_le {p b : ℤ} (hb : 0 < b) {r : ℝ} (h : ↑p ≤ ↑b * r) : ↑(p / b) ≤ r

Integer floor division rounds down in the reals.

theorem MovingSofa.GerverAreaCert.SI.le_neg_ediv_of_le {p b : ℤ} (hb : 0 < b) {r : ℝ} (h : ↑b * r ≤ ↑p) : r ≤ ↑(-(-p / b))

Integer ceiling division rounds up in the reals.

theorem MovingSofa.GerverAreaCert.SI.contains_add {x y : SI} {a b : ℝ} (hx : x.Contains a) (hy : y.Contains b) : (x.add y).Contains (a + b)

Interval addition is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_neg {x : SI} {a : ℝ} (hx : x.Contains a) : x.neg.Contains (-a)

Interval negation is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_sub {x y : SI} {a b : ℝ} (hx : x.Contains a) (hy : y.Contains b) : (x.sub y).Contains (a - b)

Interval subtraction is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_mul {x y : SI} {a b : ℝ} (hx : x.Contains a) (hy : y.Contains b) : (x.mul y).Contains (a * b)

Interval multiplication is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_divn {x : SI} {a : ℝ} {b : ℤ} (hb : 0 < b) (hx : x.Contains a) : (x.divn b).Contains (a / ↑b)

Interval division by a positive integer is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_imul {x : SI} {a : ℝ} (k : ℤ) (hx : x.Contains a) : (imul k x).Contains (↑k * a)

Interval multiplication by an integer is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_ratI {a b : ℤ} (hb : 0 < b) : (ratI a b).Contains (↑a / ↑b)

The outward enclosure of a rational is sound.

theorem MovingSofa.GerverAreaCert.SI.contains_zero : zero.Contains 0

zero encloses 0.

theorem MovingSofa.GerverAreaCert.SI.contains_one : one.Contains 1

one encloses 1.

theorem MovingSofa.GerverAreaCert.SI.contains_foldl_range {f : ℕ → SI} {g : ℕ → ℝ} (n : ℕ) (hfg : ∀ i < n, (f i).Contains (g i)) : (List.foldl (fun (acc : SI) (i : ℕ) => acc.add (f i)) zero (List.range n)).Contains (∑ i ∈ Finset.range n, g i)

A left fold of exact interval additions over an initial segment encloses the corresponding real sum.

theorem MovingSofa.GerverAreaCert.SI.foldl_range_int (f : ℕ → ℤ) (n : ℕ) : List.foldl (fun (acc : ℤ) (i : ℕ) => acc + f i) 0 (List.range n) = ∑ i ∈ Finset.range n, f i

A left fold of integer additions over an initial segment is the corresponding sum.

Certified enclosures of the twenty-two parameters and of π

def MovingSofa.GerverAreaCert.k11Z : SI

Enclosure of the direct parameter k₁₁.

Equations

• MovingSofa.GerverAreaCert.k11Z = { lo := -210322422072688751416285718490, hi := -210322422072688751416085718490 }

def MovingSofa.GerverAreaCert.k12Z : SI

Enclosure of the direct parameter k₁₂.

Equations

• MovingSofa.GerverAreaCert.k12Z = { lo := 249999999999999999999900000000, hi := 250000000000000000000100000000 }

def MovingSofa.GerverAreaCert.k21Z : SI

Enclosure of the direct parameter k₂₁.

Equations

• MovingSofa.GerverAreaCert.k21Z = { lo := -919179292771593322274796102890, hi := -919179292771593322274596102890 }

def MovingSofa.GerverAreaCert.k22Z : SI

Enclosure of the direct parameter k₂₂.

Equations

• MovingSofa.GerverAreaCert.k22Z = { lo := 472406619750805465181660762512, hi := 472406619750805465181860762512 }

def MovingSofa.GerverAreaCert.k31Z : SI

Enclosure of the direct parameter k₃₁.

Equations

• MovingSofa.GerverAreaCert.k31Z = { lo := -613763229430251668555014291320, hi := -613763229430251668554814291320 }

def MovingSofa.GerverAreaCert.k32Z : SI

Enclosure of the direct parameter k₃₂.

Equations

• MovingSofa.GerverAreaCert.k32Z = { lo := 889626479003221860726943050050, hi := 889626479003221860727143050050 }

def MovingSofa.GerverAreaCert.k41Z : SI

Enclosure of the direct parameter k₄₁.

Equations

• MovingSofa.GerverAreaCert.k41Z = { lo := -308347166088910014835232479740, hi := -308347166088910014835032479740 }

def MovingSofa.GerverAreaCert.k42Z : SI

Enclosure of the direct parameter k₄₂.

Equations

• MovingSofa.GerverAreaCert.k42Z = { lo := 472406619750805465181660762512, hi := 472406619750805465181860762512 }

def MovingSofa.GerverAreaCert.k51Z : SI

Enclosure of the direct parameter k₅₁.

Equations

• MovingSofa.GerverAreaCert.k51Z = { lo := -1017204036787814585693742864150, hi := -1017204036787814585693542864150 }

def MovingSofa.GerverAreaCert.k52Z : SI

Enclosure of the direct parameter k₅₂.

Equations

• MovingSofa.GerverAreaCert.k52Z = { lo := 249999999999999999999900000000, hi := 250000000000000000000100000000 }

def MovingSofa.GerverAreaCert.a1Z : SI

Enclosure of the direct parameter a₁.

Equations

• MovingSofa.GerverAreaCert.a1Z = { lo := 1210322422072688751416085718500, hi := 1210322422072688751416285718500 }

def MovingSofa.GerverAreaCert.a2Z : SI

Enclosure of the direct parameter a₂.

Equations

• MovingSofa.GerverAreaCert.a2Z = { lo := -250000000000000000000100000000, hi := -249999999999999999999900000000 }

def MovingSofa.GerverAreaCert.b1Z : SI

Enclosure of the direct parameter b₁.

Equations

• MovingSofa.GerverAreaCert.b1Z = { lo := -527624598026784624160603809370, hi := -527624598026784624160403809370 }

def MovingSofa.GerverAreaCert.b2Z : SI

Enclosure of the direct parameter b₂.

Equations

• MovingSofa.GerverAreaCert.b2Z = { lo := 920258385160637622893605795010, hi := 920258385160637622893805795010 }

def MovingSofa.GerverAreaCert.c1Z : SI

Enclosure of the direct parameter c₁.

Equations

• MovingSofa.GerverAreaCert.c1Z = { lo := 626045522848465867552229310386, hi := 626045522848465867552429310386 }

def MovingSofa.GerverAreaCert.c2Z : SI

Enclosure of the direct parameter c₂.

Equations

• MovingSofa.GerverAreaCert.c2Z = { lo := -944750803946430751679092381250, hi := -944750803946430751678892381250 }

def MovingSofa.GerverAreaCert.d1Z : SI

Enclosure of the direct parameter d₁.

Equations

• MovingSofa.GerverAreaCert.d1Z = { lo := 1313022761424232933776064655200, hi := 1313022761424232933776264655200 }

def MovingSofa.GerverAreaCert.d2Z : SI

Enclosure of the direct parameter d₂.

Equations

• MovingSofa.GerverAreaCert.d2Z = { lo := -525382670414554437202936294305, hi := -525382670414554437202736294305 }

def MovingSofa.GerverAreaCert.e1Z : SI

Enclosure of the direct parameter e₁.

Equations

• MovingSofa.GerverAreaCert.e1Z = { lo := 1210322422072688751416085718500, hi := 1210322422072688751416285718500 }

def MovingSofa.GerverAreaCert.e2Z : SI

Enclosure of the direct parameter e₂.

Equations

• MovingSofa.GerverAreaCert.e2Z = { lo := 249999999999999999999900000000, hi := 250000000000000000000100000000 }

def MovingSofa.GerverAreaCert.phiZ : SI

Enclosure of the first stage angle φ.

Equations

• MovingSofa.GerverAreaCert.phiZ = { lo := 39177364790083641863217874980, hi := 39177364790083641863217875500 }

def MovingSofa.GerverAreaCert.thetaZ : SI

Enclosure of the second stage angle θ.

Equations

• MovingSofa.GerverAreaCert.thetaZ = { lo := 681301509382724894473855754540, hi := 681301509382724894473855759660 }

def MovingSofa.GerverAreaCert.piZ : SI

The integer enclosure of π, from the certified Machin arctangent sums.

Equations

• MovingSofa.GerverAreaCert.piZ = { lo := 3141592653589793238462643383279, hi := 3141592653589793238462643383280 }

def MovingSofa.GerverAreaCert.piHalfZ : SI

The integer enclosure of π / 2.

Equations

• MovingSofa.GerverAreaCert.piHalfZ = MovingSofa.GerverAreaCert.piZ.divn 2

The parameter enclosures are the certified box rows

theorem MovingSofa.GerverAreaCert.contains_params : k11Z.Contains GerverSofa.PartB.params.k11 ∧ k12Z.Contains GerverSofa.PartB.params.k12 ∧ k21Z.Contains GerverSofa.PartB.params.k21 ∧ k22Z.Contains GerverSofa.PartB.params.k22 ∧ k31Z.Contains GerverSofa.PartB.params.k31 ∧ k32Z.Contains GerverSofa.PartB.params.k32 ∧ k41Z.Contains GerverSofa.PartB.params.k41 ∧ k42Z.Contains GerverSofa.PartB.params.k42 ∧ k51Z.Contains GerverSofa.PartB.params.k51 ∧ k52Z.Contains GerverSofa.PartB.params.k52 ∧ a1Z.Contains GerverSofa.PartB.params.a1 ∧ a2Z.Contains GerverSofa.PartB.params.a2 ∧ b1Z.Contains GerverSofa.PartB.params.b1 ∧ b2Z.Contains GerverSofa.PartB.params.b2 ∧ c1Z.Contains GerverSofa.PartB.params.c1 ∧ c2Z.Contains GerverSofa.PartB.params.c2 ∧ d1Z.Contains GerverSofa.PartB.params.d1 ∧ d2Z.Contains GerverSofa.PartB.params.d2 ∧ e1Z.Contains GerverSofa.PartB.params.e1 ∧ e2Z.Contains GerverSofa.PartB.params.e2 ∧ phiZ.Contains GerverSofa.PartB.params.phi ∧ thetaZ.Contains GerverSofa.PartB.params.theta

Every one of the twenty-two integer enclosures contains the corresponding certified Gerver parameter.

theorem MovingSofa.GerverAreaCert.contains_piZ : piZ.Contains Real.pi

The integer enclosure of π.

theorem MovingSofa.GerverAreaCert.contains_piHalfZ : piHalfZ.Contains (Real.pi / 2)

The integer enclosure of π / 2.

Sine and cosine by the degree-41/40 Taylor recurrence

def MovingSofa.GerverAreaCert.trigIter (z t : SI) : ℕ → SI × SI × SI × SI

trigIter z t n = (Sₙ, Cₙ, ∑_{k ≤ n} Sₖ, ∑_{k ≤ n} Cₖ) where Sₖ and Cₖ enclose the k-th signed sine and cosine Taylor terms and z encloses t ^ 2.

Equations

• One or more equations did not get rendered due to their size.
• MovingSofa.GerverAreaCert.trigIter z t 0 = (t, MovingSofa.GerverAreaCert.SI.one, t, MovingSofa.GerverAreaCert.SI.one)

def MovingSofa.GerverAreaCert.trigZ (t : SI) : SI × SI

Sine and cosine enclosures of every real number in the argument interval. Valid for arguments in [0, 2].

Equations

• One or more equations did not get rendered due to their size.

Stage endpoints and the uniform grid

def MovingSofa.GerverAreaCert.NN : ℕ

Number of subintervals per analytic stage.

Equations

• MovingSofa.GerverAreaCert.NN = 64

def MovingSofa.GerverAreaCert.endZ : ℕ → SI

Integer enclosures of the six stage endpoints 0, φ, θ, η, τ, π / 2, constant past 5.

Equations

• MovingSofa.GerverAreaCert.endZ 0 = MovingSofa.GerverAreaCert.SI.zero
• MovingSofa.GerverAreaCert.endZ 1 = MovingSofa.GerverAreaCert.phiZ
• MovingSofa.GerverAreaCert.endZ 2 = MovingSofa.GerverAreaCert.thetaZ
• MovingSofa.GerverAreaCert.endZ 3 = MovingSofa.GerverAreaCert.piHalfZ.sub MovingSofa.GerverAreaCert.thetaZ
• MovingSofa.GerverAreaCert.endZ 4 = MovingSofa.GerverAreaCert.piHalfZ.sub MovingSofa.GerverAreaCert.phiZ
• MovingSofa.GerverAreaCert.endZ x✝ = MovingSofa.GerverAreaCert.piHalfZ

def MovingSofa.GerverAreaCert.ttZ (m : ℕ) : SI

The m-th grid angle, 0 ≤ m ≤ 5 * NN.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.stageOf (m : ℕ) : ℕ

The analytic branch that the piecewise definitions select at the m-th grid angle.

Equations

• MovingSofa.GerverAreaCert.stageOf m = if m % MovingSofa.GerverAreaCert.NN = 0 then max 1 (m / MovingSofa.GerverAreaCert.NN) else m / MovingSofa.GerverAreaCert.NN + 1

The five phase formulas and the four contact curves

def MovingSofa.GerverAreaCert.evalZ (stage : ℕ) (t : SI) (kind : ℕ) : SI × SI

kind: 0 the path, 1 A, 2 B, 3 C, 4 D.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.contactZ (m kind : ℕ) : SI × SI

The contact point at grid index m, evaluated on the branch the definitions select.

Equations

• MovingSofa.GerverAreaCert.contactZ m kind = MovingSofa.GerverAreaCert.evalZ (MovingSofa.GerverAreaCert.stageOf m) (MovingSofa.GerverAreaCert.ttZ m) kind

Cap: the ordered support contacts and their fan shoelace sum

def MovingSofa.GerverAreaCert.fanCount : ℕ

Number of listed support contacts feeding the fan, excluding the anchor.

Equations

• MovingSofa.GerverAreaCert.fanCount = 10 * MovingSofa.GerverAreaCert.NN

def MovingSofa.GerverAreaCert.fanKind (i : ℕ) : ℕ

Contact kind at fan position i: A for i ≤ 5 * NN, otherwise C.

Equations

• MovingSofa.GerverAreaCert.fanKind i = if i ≤ 5 * MovingSofa.GerverAreaCert.NN then 1 else 3

def MovingSofa.GerverAreaCert.fanIdx (i : ℕ) : ℕ

Grid index at fan position i.

Equations

• MovingSofa.GerverAreaCert.fanIdx i = if i ≤ 5 * MovingSofa.GerverAreaCert.NN then i else i - 5 * MovingSofa.GerverAreaCert.NN

def MovingSofa.GerverAreaCert.fanZ (i : ℕ) : SI × SI

Both coordinates of the contact listed at fan position i.

Equations

• MovingSofa.GerverAreaCert.fanZ i = MovingSofa.GerverAreaCert.contactZ (MovingSofa.GerverAreaCert.fanIdx i) (MovingSofa.GerverAreaCert.fanKind i)

def MovingSofa.GerverAreaCert.anchorZ : SI × SI

The fan anchor L = C (π / 2).

Equations

• MovingSofa.GerverAreaCert.anchorZ = MovingSofa.GerverAreaCert.contactZ (5 * MovingSofa.GerverAreaCert.NN) 3

def MovingSofa.GerverAreaCert.crossZ (i : ℕ) : SI

The i-th fan determinant over the anchor.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.capDoubledZ : SI

Twice the signed area of the fan polygon: the shoelace sum of the listed contacts over the anchor.

Equations

• One or more equations did not get rendered due to their size.

Niche: the seven roof pieces and their covering rectangles

def MovingSofa.GerverAreaCert.rowData : ℕ → ℕ × ℕ × Bool

The seven roof pieces as (kind, stage, traversed forwards?).

Equations

• MovingSofa.GerverAreaCert.rowData 0 = (4, 1, true)
• MovingSofa.GerverAreaCert.rowData 1 = (4, 2, true)
• MovingSofa.GerverAreaCert.rowData 2 = (0, 4, false)
• MovingSofa.GerverAreaCert.rowData 3 = (0, 3, false)
• MovingSofa.GerverAreaCert.rowData 4 = (0, 2, false)
• MovingSofa.GerverAreaCert.rowData 5 = (2, 4, true)
• MovingSofa.GerverAreaCert.rowData x✝ = (2, 5, true)

def MovingSofa.GerverAreaCert.rowKind (r : ℕ) : ℕ

Contact kind traced by roof piece r.

Equations

• MovingSofa.GerverAreaCert.rowKind r = (MovingSofa.GerverAreaCert.rowData r).1

def MovingSofa.GerverAreaCert.rowStage (r : ℕ) : ℕ

Analytic stage traced by roof piece r.

Equations

• MovingSofa.GerverAreaCert.rowStage r = (MovingSofa.GerverAreaCert.rowData r).2.1

def MovingSofa.GerverAreaCert.rowFwd (r : ℕ) : Bool

Whether roof piece r is traversed in increasing time.

Equations

• MovingSofa.GerverAreaCert.rowFwd r = (MovingSofa.GerverAreaCert.rowData r).2.2

def MovingSofa.GerverAreaCert.rowBase (r j : ℕ) : ℕ

Grid index of the left end of the j-th subinterval of row r.

Equations

• MovingSofa.GerverAreaCert.rowBase r j = (MovingSofa.GerverAreaCert.rowStage r - 1) * MovingSofa.GerverAreaCert.NN + j

def MovingSofa.GerverAreaCert.rectLoZ (r j : ℕ) : ℤ

Left horizontal bound of the covering rectangle of (r, j).

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.rectHiZ (r j : ℕ) : ℤ

Right horizontal bound of the covering rectangle of (r, j).

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.rectHZ (r j : ℕ) : ℤ

Height bound of the covering rectangle of (r, j): the branch evaluation over the whole subinterval, widened to cover the left endpoint, which sits on the previous branch.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.rectAreaZ (r j : ℕ) : ℤ

Area of the covering rectangle of (r, j), in units of 1 / M ^ 2.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerverAreaCert.rowSumZ (r : ℕ) : ℤ

Total covering area of row r, in units of 1 / M ^ 2.

Equations

• MovingSofa.GerverAreaCert.rowSumZ r = List.foldl (fun (acc : ℤ) (j : ℕ) => acc + MovingSofa.GerverAreaCert.rectAreaZ r j) 0 (List.range MovingSofa.GerverAreaCert.NN)

def MovingSofa.GerverAreaCert.nicheSumZ : ℤ

Total covering area of the 7 * NN rectangles, in units of 1 / M ^ 2.

Equations

• MovingSofa.GerverAreaCert.nicheSumZ = List.foldl (fun (acc : ℤ) (r : ℕ) => acc + MovingSofa.GerverAreaCert.rowSumZ r) 0 (List.range 7)

The two decidable numeric conclusions

def MovingSofa.GerverAreaCert.capOK : Bool

The closed numeric cap check: 2 * 28609 / 10000 ≤ capDoubledZ.lo / M.

def MovingSofa.GerverAreaCert.nicheOK : Bool

The closed numeric niche check: nicheSumZ / M ^ 2 ≤ 3301 / 5000.

theorem MovingSofa.GerverAreaCert.nicheOK_true : nicheOK = true

The niche check passes, by kernel reduction.

theorem MovingSofa.GerverAreaCert.capOK_true : capOK = true

The cap check passes, by kernel reduction.

Interval enclosures of the sine and cosine at scale M

The certificate evaluates the sine and the cosine by the interval Taylor recurrence GerverAreaCert.trigIter, truncated at degree 41 and 40 and widened by one unit at scale M = 10 ^ 30. trigZ_sound is the soundness statement of that evaluator on [0, 2]: the recurrence encloses the signed Taylor terms and their partial sums (contains_trigIter), the alternating brackets of Real.sin and Real.cos control the truncation error by the first omitted term, and 2 ^ 41 * 10 ^ 30 ≤ 41! and 2 ^ 40 * 10 ^ 30 ≤ 40! justify the one-unit widening.

Sine and cosine enclosures

theorem MovingSofa.contains_trigIter {z t : GerverAreaCert.SI} {x : ℝ} (hz : z.Contains (x * x)) (ht : t.Contains x) (n : ℕ) : (GerverAreaCert.trigIter z t n).1.Contains ((-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1).factorial) ∧ (GerverAreaCert.trigIter z t n).2.1.Contains ((-1) ^ n * x ^ (2 * n) / ↑(2 * n).factorial) ∧ (GerverAreaCert.trigIter z t n).2.2.1.Contains (∑ k ∈ Finset.range (n + 1), (-1) ^ k * x ^ (2 * k + 1) / ↑(2 * k + 1).factorial) ∧ (GerverAreaCert.trigIter z t n).2.2.2.Contains (∑ k ∈ Finset.range (n + 1), (-1) ^ k * x ^ (2 * k) / ↑(2 * k).factorial)

The integer term recurrence encloses the signed Taylor terms and their partial sums. Pure interval arithmetic: an induction on n using the SI soundness lemmas.

theorem MovingSofa.trigZ_sound {t : GerverAreaCert.SI} {x : ℝ} (ht : t.Contains x) (hx0 : 0 ≤ x) (hx2 : x ≤ 2) : (GerverAreaCert.trigZ t).1.Contains (Real.sin x) ∧ (GerverAreaCert.trigZ t).2.Contains (Real.cos x)

Soundness of the executable sine/cosine enclosure on [0, 2].