Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.Foundation.Batch003.
• GerverSofa.KernelOnly.Numerics.Batch001.
• GerverSofa.KernelOnly.Numerics.Batch002.
• GerverSofa.KernelOnly.Numerics.Batch003.
• GerverSofa.KernelOnly.Numerics.Batch004.
• GerverSofa.KernelOnly.Numerics.Batch005.
• GerverSofa.KernelOnly.Foundation.Batch004.
• GerverSofa.KernelOnly.PartE.Semantics.Batch001.
• GerverSofa.KernelOnly.PartB.Semantics.Batch003.

Gerver sofa dependency batch

• KernelOnly.JacobianCache.
• KernelOnly.LeanCertGerverNumericsReduced.

Shared exact interval Jacobian for the 22-dimensional certificate

The kernel verifies every matrix entry against the original automatic differentiation evaluator. Matrix row bounds can then reuse the certified entries.

def GerverSofa.PartALeanCert.naturalFromChunks (chunks : List ℕ) : ℕ

Reconstruct a natural number from base-10³⁵ chunks for decimal elaboration.

Equations

• GerverSofa.PartALeanCert.naturalFromChunks chunks = List.foldl (fun (value digit : ℕ) => value * 10 ^ 35 + digit) 0 chunks

def GerverSofa.PartALeanCert.jacobianEntry000 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 0, shared by equal entries.

Equations

• GerverSofa.PartALeanCert.jacobianEntry000 = { lo := GerverSofa.PartALeanCert.q 0 1, hi := GerverSofa.PartALeanCert.q 0 1, le := GerverSofa.PartALeanCert.jacobianEntry000._proof_2 }

def GerverSofa.PartALeanCert.jacobianEntry001 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 1, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry002 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 2, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry003 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 3, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry004 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 4, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry005 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 5, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry006 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 6, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry007 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 7, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry008 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 8, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry009 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 9, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry010 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 10, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry011 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 11, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry012 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 12, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry013 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 13, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry014 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 14, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry015 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 15, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry016 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 16, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry017 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 17, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry018 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 18, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry019 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 19, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry020 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 20, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry021 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 21, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry022 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 22, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry023 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 23, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry024 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 24, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry025 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 25, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry026 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 26, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry027 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 27, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry028 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 28, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry029 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 29, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry030 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 30, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry031 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 31, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry032 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 32, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry033 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 33, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry034 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 34, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry035 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 35, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry036 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 36, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry037 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 37, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry038 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 38, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry039 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 39, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry040 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 40, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry041 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 41, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry042 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 42, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry043 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 43, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry044 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 44, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry045 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 45, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry046 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 46, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry047 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 47, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry048 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 48, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry049 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 49, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry050 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 50, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry051 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 51, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry052 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 52, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry053 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 53, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry054 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 54, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianEntry055 : LeanCert.Core.IntervalRat

Exact cached Jacobian interval number 55, shared by equal entries.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow00 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 0 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow01 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 1 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow02 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 2 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow03 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 3 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow04 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 4 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow05 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 5 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow06 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 6 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow07 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 7 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow08 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 8 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow09 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 9 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow10 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 10 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow11 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 11 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow12 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 12 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow13 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 13 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow14 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 14 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow15 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 15 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow16 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 16 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow17 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 17 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow18 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 18 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow19 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 19 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow20 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 20 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianRow21 (j : Fin 22) : LeanCert.Core.IntervalRat

Cached interval row 21 of the full Jacobian.

Equations

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

def GerverSofa.PartALeanCert.jacobianCache (i j : Fin 22) : LeanCert.Core.IntervalRat

Select an exact cached interval from the full interval Jacobian.

Equations

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

theorem GerverSofa.PartALeanCert.jacobianRow00_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 0 j = jacobianCache 0 j

theorem GerverSofa.PartALeanCert.jacobianRow01_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 1 j = jacobianCache 1 j

theorem GerverSofa.PartALeanCert.jacobianRow02_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 2 j = jacobianCache 2 j

theorem GerverSofa.PartALeanCert.jacobianRow03_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 3 j = jacobianCache 3 j

theorem GerverSofa.PartALeanCert.jacobianRow04_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 4 j = jacobianCache 4 j

theorem GerverSofa.PartALeanCert.jacobianRow05_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 5 j = jacobianCache 5 j

theorem GerverSofa.PartALeanCert.jacobianRow06_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 6 j = jacobianCache 6 j

theorem GerverSofa.PartALeanCert.jacobianRow07_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 7 j = jacobianCache 7 j

theorem GerverSofa.PartALeanCert.jacobianRow08_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 8 j = jacobianCache 8 j

theorem GerverSofa.PartALeanCert.jacobianRow09_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 9 j = jacobianCache 9 j

theorem GerverSofa.PartALeanCert.jacobianRow10_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 10 j = jacobianCache 10 j

theorem GerverSofa.PartALeanCert.jacobianRow11_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 11 j = jacobianCache 11 j

theorem GerverSofa.PartALeanCert.jacobianRow12_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 12 j = jacobianCache 12 j

theorem GerverSofa.PartALeanCert.jacobianRow13_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 13 j = jacobianCache 13 j

theorem GerverSofa.PartALeanCert.jacobianRow14_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 14 j = jacobianCache 14 j

theorem GerverSofa.PartALeanCert.jacobianRow15_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 15 j = jacobianCache 15 j

theorem GerverSofa.PartALeanCert.jacobianRow16_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 16 j = jacobianCache 16 j

theorem GerverSofa.PartALeanCert.jacobianRow17_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 17 j = jacobianCache 17 j

theorem GerverSofa.PartALeanCert.jacobianRow18_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 18 j = jacobianCache 18 j

theorem GerverSofa.PartALeanCert.jacobianRow19_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 19 j = jacobianCache 19 j

theorem GerverSofa.PartALeanCert.jacobianRow20_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 20 j = jacobianCache 20 j

theorem GerverSofa.PartALeanCert.jacobianRow21_eq (j : Fin 22) : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg 21 j = jacobianCache 21 j

theorem GerverSofa.PartALeanCert.jacobianCache_eq : LeanCert.Engine.intervalJacobian fullExpr unitBox cfg = jacobianCache

Gerver Sofa / Kernel Only / Lean Cert Gerver Numerics Reduced

theorem GerverSofa.PartALeanCert.reduced_row_0_lt : LeanCert.Engine.intervalMatrixRowBound reducedPJ 0 < qTarget

theorem GerverSofa.PartALeanCert.reduced_row_1_lt : LeanCert.Engine.intervalMatrixRowBound reducedPJ 1 < qTarget

theorem GerverSofa.PartALeanCert.reduced_row_2_lt : LeanCert.Engine.intervalMatrixRowBound reducedPJ 2 < qTarget

theorem GerverSofa.PartALeanCert.reduced_row_3_lt : LeanCert.Engine.intervalMatrixRowBound reducedPJ 3 < qTarget

theorem GerverSofa.PartALeanCert.reduced_bound_lt : LeanCert.Engine.intervalMatrixBound reducedPJ < qTarget

theorem GerverSofa.PartALeanCert.reduced_bound_le : LeanCert.Engine.intervalMatrixBound reducedPJ ≤ qTarget

theorem GerverSofa.PartALeanCert.reduced_image_0_inside : LeanCert.Engine.intervalStrictInside (reducedImageQ 0) (unitBox 0) = true

theorem GerverSofa.PartALeanCert.reduced_image_1_inside : LeanCert.Engine.intervalStrictInside (reducedImageQ 1) (unitBox 1) = true

theorem GerverSofa.PartALeanCert.reduced_image_2_inside : LeanCert.Engine.intervalStrictInside (reducedImageQ 2) (unitBox 2) = true

theorem GerverSofa.PartALeanCert.reduced_image_3_inside : LeanCert.Engine.intervalStrictInside (reducedImageQ 3) (unitBox 3) = true

theorem GerverSofa.PartALeanCert.reduced_images_inside (i : Fin 4) : LeanCert.Engine.intervalStrictInside (reducedImageQ i) (unitBox i) = true

theorem GerverSofa.PartALeanCert.reduced_unique_scaled : ∃! u : Fin 4 → ℝ, LeanCert.Engine.FinBoxMem u unitBox ∧ LeanCert.Engine.SystemZero reducedExpr u

Gerver sofa dependency batch

• KernelOnly.LeanCertNumericsRows.Full00.
• KernelOnly.LeanCertNumericsRows.FullPoint00.
• KernelOnly.LeanCertNumericsRows.FullImage00.
• KernelOnly.LeanCertNumericsRows.Full01.
• KernelOnly.LeanCertNumericsRows.FullPoint01.
• KernelOnly.LeanCertNumericsRows.FullImage01.
• KernelOnly.LeanCertNumericsRows.Full02.
• KernelOnly.LeanCertNumericsRows.FullPoint02.
• KernelOnly.LeanCertNumericsRows.FullImage02.
• KernelOnly.LeanCertNumericsRows.Full03.
• KernelOnly.LeanCertNumericsRows.FullPoint03.
• KernelOnly.LeanCertNumericsRows.FullImage03.
• KernelOnly.LeanCertNumericsRows.Full04.
• KernelOnly.LeanCertNumericsRows.FullPoint04.
• KernelOnly.LeanCertNumericsRows.FullImage04.
• KernelOnly.LeanCertNumericsRows.Full05.

Direct 22D certificate, row 0: Jacobian bound

The row modules form a deliberate dependency chain beginning after the already-certified reduced 4D module. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_0_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 0 < qTarget

Direct 22D certificate, point residual 0

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_0_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 0) (fullPointCache 0)

theorem GerverSofa.PartALeanCert.full_point_0_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 0 ∈ fullPointCache 0

Direct 22D certificate, row 0: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_0_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 0) (unitBox 0) = true

Direct 22D certificate, row 1: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_1_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 1 < qTarget

Direct 22D certificate, point residual 1

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_1_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 1) (fullPointCache 1)

theorem GerverSofa.PartALeanCert.full_point_1_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 1 ∈ fullPointCache 1

Direct 22D certificate, row 1: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_1_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 1) (unitBox 1) = true

Direct 22D certificate, row 2: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_2_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 2 < qTarget

Direct 22D certificate, point residual 2

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_2_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 2) (fullPointCache 2)

theorem GerverSofa.PartALeanCert.full_point_2_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 2 ∈ fullPointCache 2

Direct 22D certificate, row 2: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_2_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 2) (unitBox 2) = true

Direct 22D certificate, row 3: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_3_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 3 < qTarget

Direct 22D certificate, point residual 3

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_3_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 3) (fullPointCache 3)

theorem GerverSofa.PartALeanCert.full_point_3_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 3 ∈ fullPointCache 3

Direct 22D certificate, row 3: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_3_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 3) (unitBox 3) = true

Direct 22D certificate, row 4: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_4_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 4 < qTarget

Direct 22D certificate, point residual 4

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_4_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 4) (fullPointCache 4)

theorem GerverSofa.PartALeanCert.full_point_4_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 4 ∈ fullPointCache 4

Direct 22D certificate, row 4: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_4_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 4) (unitBox 4) = true

Direct 22D certificate, row 5: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_5_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 5 < qTarget

Gerver sofa dependency batch

• KernelOnly.LeanCertNumericsRows.FullPoint05.
• KernelOnly.LeanCertNumericsRows.FullImage05.
• KernelOnly.LeanCertNumericsRows.Full06.
• KernelOnly.LeanCertNumericsRows.FullPoint06.
• KernelOnly.LeanCertNumericsRows.FullImage06.
• KernelOnly.LeanCertNumericsRows.Full07.
• KernelOnly.LeanCertNumericsRows.FullPoint07.
• KernelOnly.LeanCertNumericsRows.FullImage07.
• KernelOnly.LeanCertNumericsRows.Full08.
• KernelOnly.LeanCertNumericsRows.FullPoint08.
• KernelOnly.LeanCertNumericsRows.FullImage08.
• KernelOnly.LeanCertNumericsRows.Full09.
• KernelOnly.LeanCertNumericsRows.FullPoint09.
• KernelOnly.LeanCertNumericsRows.FullImage09.
• KernelOnly.LeanCertNumericsRows.Full10.
• KernelOnly.LeanCertNumericsRows.FullPoint10.

Direct 22D certificate, point residual 5

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_5_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 5) (fullPointCache 5)

theorem GerverSofa.PartALeanCert.full_point_5_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 5 ∈ fullPointCache 5

Direct 22D certificate, row 5: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_5_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 5) (unitBox 5) = true

Direct 22D certificate, row 6: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_6_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 6 < qTarget

Direct 22D certificate, point residual 6

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_6_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 6) (fullPointCache 6)

theorem GerverSofa.PartALeanCert.full_point_6_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 6 ∈ fullPointCache 6

Direct 22D certificate, row 6: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_6_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 6) (unitBox 6) = true

Direct 22D certificate, row 7: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_7_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 7 < qTarget

Direct 22D certificate, point residual 7

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_7_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 7) (fullPointCache 7)

theorem GerverSofa.PartALeanCert.full_point_7_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 7 ∈ fullPointCache 7

Direct 22D certificate, row 7: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_7_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 7) (unitBox 7) = true

Direct 22D certificate, row 8: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_8_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 8 < qTarget

Direct 22D certificate, point residual 8

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_8_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 8) (fullPointCache 8)

theorem GerverSofa.PartALeanCert.full_point_8_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 8 ∈ fullPointCache 8

Direct 22D certificate, row 8: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_8_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 8) (unitBox 8) = true

Direct 22D certificate, row 9: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_9_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 9 < qTarget

Direct 22D certificate, point residual 9

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_9_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 9) (fullPointCache 9)

theorem GerverSofa.PartALeanCert.full_point_9_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 9 ∈ fullPointCache 9

Direct 22D certificate, row 9: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_9_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 9) (unitBox 9) = true

Direct 22D certificate, row 10: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_10_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 10 < qTarget

Direct 22D certificate, point residual 10

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_10_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 10) (fullPointCache 10)

theorem GerverSofa.PartALeanCert.full_point_10_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 10 ∈ fullPointCache 10

Gerver sofa dependency batch

• KernelOnly.LeanCertNumericsRows.FullImage10.
• KernelOnly.LeanCertNumericsRows.Full11.
• KernelOnly.LeanCertNumericsRows.FullPoint11.
• KernelOnly.LeanCertNumericsRows.FullImage11.
• KernelOnly.LeanCertNumericsRows.Full12.
• KernelOnly.LeanCertNumericsRows.FullPoint12.
• KernelOnly.LeanCertNumericsRows.FullImage12.
• KernelOnly.LeanCertNumericsRows.Full13.
• KernelOnly.LeanCertNumericsRows.FullPoint13.
• KernelOnly.LeanCertNumericsRows.FullImage13.
• KernelOnly.LeanCertNumericsRows.Full14.
• KernelOnly.LeanCertNumericsRows.FullPoint14.
• KernelOnly.LeanCertNumericsRows.FullImage14.
• KernelOnly.LeanCertNumericsRows.Full15.
• KernelOnly.LeanCertNumericsRows.FullPoint15.
• KernelOnly.LeanCertNumericsRows.FullImage15.

Direct 22D certificate, row 10: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_10_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 10) (unitBox 10) = true

Direct 22D certificate, row 11: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_11_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 11 < qTarget

Direct 22D certificate, point residual 11

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_11_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 11) (fullPointCache 11)

theorem GerverSofa.PartALeanCert.full_point_11_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 11 ∈ fullPointCache 11

Direct 22D certificate, row 11: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_11_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 11) (unitBox 11) = true

Direct 22D certificate, row 12: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_12_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 12 < qTarget

Direct 22D certificate, point residual 12

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_12_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 12) (fullPointCache 12)

theorem GerverSofa.PartALeanCert.full_point_12_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 12 ∈ fullPointCache 12

Direct 22D certificate, row 12: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_12_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 12) (unitBox 12) = true

Direct 22D certificate, row 13: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_13_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 13 < qTarget

Direct 22D certificate, point residual 13

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_13_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 13) (fullPointCache 13)

theorem GerverSofa.PartALeanCert.full_point_13_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 13 ∈ fullPointCache 13

Direct 22D certificate, row 13: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_13_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 13) (unitBox 13) = true

Direct 22D certificate, row 14: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_14_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 14 < qTarget

Direct 22D certificate, point residual 14

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_14_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 14) (fullPointCache 14)

theorem GerverSofa.PartALeanCert.full_point_14_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 14 ∈ fullPointCache 14

Direct 22D certificate, row 14: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_14_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 14) (unitBox 14) = true

Direct 22D certificate, row 15: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_15_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 15 < qTarget

Direct 22D certificate, point residual 15

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_15_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 15) (fullPointCache 15)

theorem GerverSofa.PartALeanCert.full_point_15_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 15 ∈ fullPointCache 15

Direct 22D certificate, row 15: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_15_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 15) (unitBox 15) = true

Gerver sofa dependency batch

• KernelOnly.LeanCertNumericsRows.Full16.
• KernelOnly.LeanCertNumericsRows.FullPoint16.
• KernelOnly.LeanCertNumericsRows.FullImage16.
• KernelOnly.LeanCertNumericsRows.Full17.
• KernelOnly.LeanCertNumericsRows.FullPoint17.
• KernelOnly.LeanCertNumericsRows.FullImage17.
• KernelOnly.LeanCertNumericsRows.Full18.
• KernelOnly.LeanCertNumericsRows.FullPoint18.
• KernelOnly.LeanCertNumericsRows.FullImage18.
• KernelOnly.LeanCertNumericsRows.Full19.
• KernelOnly.LeanCertNumericsRows.FullPoint19.
• KernelOnly.LeanCertNumericsRows.FullImage19.
• KernelOnly.LeanCertNumericsRows.Full20.
• KernelOnly.LeanCertNumericsRows.FullPoint20.
• KernelOnly.LeanCertNumericsRows.FullImage20.
• KernelOnly.LeanCertNumericsRows.Full21.

Direct 22D certificate, row 16: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_16_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 16 < qTarget

Direct 22D certificate, point residual 16

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_16_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 16) (fullPointCache 16)

theorem GerverSofa.PartALeanCert.full_point_16_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 16 ∈ fullPointCache 16

Direct 22D certificate, row 16: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_16_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 16) (unitBox 16) = true

Direct 22D certificate, row 17: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_17_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 17 < qTarget

Direct 22D certificate, point residual 17

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_17_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 17) (fullPointCache 17)

theorem GerverSofa.PartALeanCert.full_point_17_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 17 ∈ fullPointCache 17

Direct 22D certificate, row 17: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_17_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 17) (unitBox 17) = true

Direct 22D certificate, row 18: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_18_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 18 < qTarget

Direct 22D certificate, point residual 18

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_18_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 18) (fullPointCache 18)

theorem GerverSofa.PartALeanCert.full_point_18_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 18 ∈ fullPointCache 18

Direct 22D certificate, row 18: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_18_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 18) (unitBox 18) = true

Direct 22D certificate, row 19: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_19_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 19 < qTarget

Direct 22D certificate, point residual 19

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_19_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 19) (fullPointCache 19)

theorem GerverSofa.PartALeanCert.full_point_19_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 19 ∈ fullPointCache 19

Direct 22D certificate, row 19: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_19_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 19) (unitBox 19) = true

Direct 22D certificate, row 20: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_20_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 20 < qTarget

Direct 22D certificate, point residual 20

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_20_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 20) (fullPointCache 20)

theorem GerverSofa.PartALeanCert.full_point_20_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 20 ∈ fullPointCache 20

Direct 22D certificate, row 20: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_20_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 20) (unitBox 20) = true

Direct 22D certificate, row 21: Jacobian bound

The row modules form a deliberate dependency chain. Lake therefore checks only one expensive closed kernel proposition at a time instead of launching all 22 rows concurrently and exhausting RAM.

theorem GerverSofa.PartALeanCert.full_row_21_lt : LeanCert.Engine.intervalMatrixRowBound fullPJ 21 < qTarget

Gerver sofa dependency batch

• KernelOnly.LeanCertNumericsRows.FullPoint21.
• KernelOnly.LeanCertNumericsRows.FullImage21.

Direct 22D certificate, point residual 21

The expensive transcendental evaluation is checked once for this single coordinate and then replaced by a small rational cache interval downstream.

theorem GerverSofa.PartALeanCert.full_point_21_contained : intervalContained (pointEvalIntervalsKernel fullExpr zeroCenter cfg 21) (fullPointCache 21)

theorem GerverSofa.PartALeanCert.full_point_21_mem : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) 21 ∈ fullPointCache 21

Direct 22D certificate, row 21: strict self-map image

This theorem is isolated from the Jacobian-row theorem so each Lean process checks one heavy proposition and then releases its memory before the next module in the serial chain begins.

theorem GerverSofa.PartALeanCert.full_image_21_inside : LeanCert.Engine.intervalStrictInside (fullImageCachedQ 21) (unitBox 21) = true

Gerver sofa dependency batch

• KernelOnly.LeanCertGerverNumerics.
• KernelOnly.ConcreteUniqueZeros.

Final LeanCert numerical certificate for Gerver

All expensive 22D checks are already cached in a serial dependency chain ending at FullImage21. This module only assembles them into the global norm/self-map facts and the unique-root theorem.

theorem GerverSofa.PartALeanCert.full_bound_lt : LeanCert.Engine.intervalMatrixBound fullPJ < qTarget

theorem GerverSofa.PartALeanCert.full_bound_le : LeanCert.Engine.intervalMatrixBound fullPJ ≤ qTarget

theorem GerverSofa.PartALeanCert.full_point_values_mem (j : Fin 22) : LeanCert.Engine.systemEval fullExpr (fun (k : Fin 22) => ↑(zeroCenter k)) j ∈ fullPointCache j

theorem GerverSofa.PartALeanCert.full_images_inside (i : Fin 22) : LeanCert.Engine.intervalStrictInside (fullImageCachedQ i) (unitBox i) = true

theorem GerverSofa.PartALeanCert.full_unique_scaled : ∃! u : Fin 22 → ℝ, LeanCert.Engine.FinBoxMem u unitBox ∧ LeanCert.Engine.SystemZero fullExpr u

Gerver Sofa / Kernel Only / Concrete Unique Zeros

noncomputable def GerverSofa.PartALeanCert.reducedRootU : Fin 4 → ℝ

The unique normalized reduced-system zero selected from its existence certificate.

Equations

• GerverSofa.PartALeanCert.reducedRootU = Classical.choose GerverSofa.PartALeanCert.reduced_unique_scaled

noncomputable def GerverSofa.PartALeanCert.fullRootU : Fin 22 → ℝ

The unique normalized full-system zero selected from its existence certificate.

Equations

• GerverSofa.PartALeanCert.fullRootU = Classical.choose GerverSofa.PartALeanCert.full_unique_scaled

theorem GerverSofa.PartALeanCert.reducedRootU_spec : LeanCert.Engine.FinBoxMem reducedRootU unitBox ∧ LeanCert.Engine.SystemZero reducedExpr reducedRootU

theorem GerverSofa.PartALeanCert.fullRootU_spec : LeanCert.Engine.FinBoxMem fullRootU unitBox ∧ LeanCert.Engine.SystemZero fullExpr fullRootU

noncomputable def GerverSofa.PartALeanCert.reducedRoot : Vec 4

The certified reduced-system root in the original box coordinates.

Equations

• GerverSofa.PartALeanCert.reducedRoot = GerverSofa.PartALeanCert.reducedAffine GerverSofa.PartALeanCert.reducedRootU

noncomputable def GerverSofa.PartALeanCert.fullRoot : Vec 22

The certified full-system root in the original Romik parameter coordinates.

Equations

• GerverSofa.PartALeanCert.fullRoot = GerverSofa.PartALeanCert.fullAffine GerverSofa.PartALeanCert.fullRootU

theorem GerverSofa.PartALeanCert.reducedRoot_mem : reducedRoot ∈ Reduced.vectorBox

theorem GerverSofa.PartALeanCert.fullRoot_mem : fullRoot ∈ Romik.vectorBox

theorem GerverSofa.PartALeanCert.reducedRoot_zero : Reduced.vectorSystem reducedRoot = 0

theorem GerverSofa.PartALeanCert.fullRoot_zero : Romik.vectorSystem fullRoot = 0

noncomputable def GerverSofa.PartALeanCert.reducedCertifiedUniqueZero : CertifiedUniqueZero Reduced.vectorSystem Reduced.vectorBox

Concrete reduced 4D unique zero — no assumptions.

Equations

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

noncomputable def GerverSofa.PartALeanCert.reducedCertifiedUniqueSolution : CertifiedUniqueSolution Reduced.Equations Reduced.box

Existing manuscript-level unique-solution interfaces are now discharged by concrete numerical certificates rather than assumptions.

Equations

• GerverSofa.PartALeanCert.reducedCertifiedUniqueSolution = GerverSofa.Reduced.uniqueSolutionOfVector GerverSofa.PartALeanCert.reducedCertifiedUniqueZero

Gerver sofa dependency batch

• KernelOnly.PartE.DeepMindABPhiThetaBridge.
• KernelOnly.PartE.TwoAngleReduction.
• KernelOnly.PartE.ScaledResidualInterval.
• KernelOnly.PartE.FiniteCoverReplay.
• KernelOnly.PartE.LocalTwoAngleKrawczykClosure.
• KernelOnly.PartE.AdaptiveGlobalCoverClosure.
• KernelOnly.PartE.E24AlignedRegionFoundation.
• KernelOnly.PartE.E24AlignedLogic.
• KernelOnly.PartE.E24KC2ProofHelpers.
• KernelOnly.PartE.E24PhiBelowKernelHL.

Part E01: bridge to DeepMind's Gerver-constant specification

This module mirrors the four equations and the physical domain used by GerversSofa.ABφθSpec in google-deepmind/formal-conjectures. It proves that the four displayed equations are exactly the already certified reduced Gerver system, proves that the certified rational box lies in the physical domain, and reduces the tuple-shaped global uniqueness statement to one explicit global enclosure target.

The enclosure target is a proposition passed as an ordinary theorem argument. E01 does not claim that the global exclusion step has already been proved.

def GerverSofa.PartE.reducedParams (A B phi theta : ℝ) : Reduced.Params

Reduced parameters assembled in the order (A, B, phi, theta).

Equations

• GerverSofa.PartE.reducedParams A B phi theta = { a := A, b := B, phi := phi, theta := theta }

def GerverSofa.PartE.PhysicalDomain (p : Reduced.Params) : Prop

The physical domain appearing in DeepMind's ABφθSpec.

Equations

• GerverSofa.PartE.PhysicalDomain p = (0 ≤ p.phi ∧ p.phi ≤ p.theta ∧ p.theta ≤ Real.pi / 4 ∧ 0 ≤ p.a ∧ 0 ≤ p.b)

def GerverSofa.PartE.DeepMindEquations (A B phi theta : ℝ) : Prop

The four displayed equations in DeepMind's ABφθSpec.

Equations

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

def GerverSofa.PartE.DeepMindABPhiThetaSpec (A B phi theta : ℝ) : Prop

A local mirror of DeepMind's complete four-constant specification.

Equations

• GerverSofa.PartE.DeepMindABPhiThetaSpec A B phi theta = (GerverSofa.PartE.PhysicalDomain (GerverSofa.PartE.reducedParams A B phi theta) ∧ GerverSofa.PartE.DeepMindEquations A B phi theta)

theorem GerverSofa.PartE.deepMindEquations_iff_reducedEquations (A B phi theta : ℝ) : DeepMindEquations A B phi theta ↔ Reduced.Equations (reducedParams A B phi theta)

Explicit equivalence between DeepMind's four equations and the certified reduced Gerver system.

theorem GerverSofa.PartE.physicalDomain_of_mem_reducedBox {p : Reduced.Params} (hp : p ∈ Reduced.box) : PhysicalDomain p

Every point of the certified reduced box satisfies DeepMind's broad physical-domain inequalities.

theorem GerverSofa.PartE.deepMindSpec_iff_physicalDomain_and_reducedEquations (A B phi theta : ℝ) : DeepMindABPhiThetaSpec A B phi theta ↔ PhysicalDomain (reducedParams A B phi theta) ∧ Reduced.Equations (reducedParams A B phi theta)

The mirrored DeepMind specification is precisely physical-domain membership plus the already named reduced equations.

theorem GerverSofa.PartE.deepMindSpec_of_mem_reducedBox_and_equations {p : Reduced.Params} (hp : p ∈ Reduced.box) (heq : Reduced.Equations p) : DeepMindABPhiThetaSpec p.a p.b p.phi p.theta

A certified-box solution of the reduced system is automatically a solution of the mirrored DeepMind specification.

def GerverSofa.PartE.GlobalEnclosureTarget : Prop

The sole new mathematical target left after E01: every physical solution of the reduced equations lies in the already certified rational box.

Equations

• GerverSofa.PartE.GlobalEnclosureTarget = ∀ (p : GerverSofa.Reduced.Params), GerverSofa.PartE.PhysicalDomain p → GerverSofa.Reduced.Equations p → p ∈ GerverSofa.Reduced.box

def GerverSofa.PartE.tupleEquiv : ℝ × ℝ × ℝ × ℝ ≃ Reduced.Params

Coordinate equivalence between DeepMind's nested tuple and the named reduced-parameter record.

Equations

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

theorem GerverSofa.PartE.deepMindABPhiTheta_existsUnique_of_globalEnclosure (hglobal : GlobalEnclosureTarget) : ∃! ABphiTheta : ℝ × ℝ × ℝ × ℝ, DeepMindABPhiThetaSpec ABphiTheta.1 ABphiTheta.2.1 ABphiTheta.2.2.1 ABphiTheta.2.2.2

Once the explicit global enclosure theorem is supplied, the existing kernel-checked local certificate yields the exact tuple-shaped uniqueness statement required by DeepMind.

Part E02: exact reduction of the DeepMind system to two angles

E01 identified the sole missing mathematical input as a global enclosure of all physical solutions of the four-variable reduced system. E02 eliminates the two linear variables A and B exactly.

The third and fourth Gerver equations first give B as an affine expression in A, and then give A as a quotient depending only on (phi, theta). The denominator is proved nonzero for every physical solution; this is a theorem, not an additional assumption. Consequently existence of a physical four-variable solution is equivalent to a two-angle specification.

The remaining enclosure target quantifies only over 0 <= phi <= theta <= pi/4. It is still an ordinary theorem argument: E02 does not declare the interval branch-and-bound conclusion as an axiom.

def GerverSofa.PartE.angleDelta (phi theta : ℝ) : ℝ

Difference of the two switching angles.

Equations

• GerverSofa.PartE.angleDelta phi theta = theta - phi

noncomputable def GerverSofa.PartE.bBase (phi theta : ℝ) : ℝ

Constant part of the fourth equation after solving it for B.

Equations

• GerverSofa.PartE.bBase phi theta = Real.pi / 2 - phi - theta + GerverSofa.PartE.angleDelta phi theta / 2 + GerverSofa.PartE.angleDelta phi theta ^ 2 / 4

noncomputable def GerverSofa.PartE.bFromA (A phi theta : ℝ) : ℝ

The value of B forced by the fourth equation once A is fixed.

Equations

• GerverSofa.PartE.bFromA A phi theta = A * (1 + GerverSofa.PartE.angleDelta phi theta / 2) + GerverSofa.PartE.bBase phi theta

noncomputable def GerverSofa.PartE.angleDenominator (phi theta : ℝ) : ℝ

Denominator obtained from the third equation after eliminating B.

Equations

• GerverSofa.PartE.angleDenominator phi theta = Real.cos phi - (1 + GerverSofa.PartE.angleDelta phi theta / 2) * Real.sin phi

noncomputable def GerverSofa.PartE.angleNumerator (phi theta : ℝ) : ℝ

Numerator obtained from the third equation after eliminating B.

Equations

• GerverSofa.PartE.angleNumerator phi theta = Real.sin phi + 1 / 2 - Real.cos phi / 2 + GerverSofa.PartE.bBase phi theta * Real.sin phi

noncomputable def GerverSofa.PartE.reconstructedA (phi theta : ℝ) : ℝ

Reconstructed value of A, depending only on the two angles.

Equations

• GerverSofa.PartE.reconstructedA phi theta = GerverSofa.PartE.angleNumerator phi theta / GerverSofa.PartE.angleDenominator phi theta

noncomputable def GerverSofa.PartE.reconstructedB (phi theta : ℝ) : ℝ

Reconstructed value of B, depending only on the two angles.

Equations

• GerverSofa.PartE.reconstructedB phi theta = GerverSofa.PartE.bFromA (GerverSofa.PartE.reconstructedA phi theta) phi theta

def GerverSofa.PartE.PhysicalAngleDomain (phi theta : ℝ) : Prop

The triangular physical domain for the two switching angles.

Equations

• GerverSofa.PartE.PhysicalAngleDomain phi theta = (0 ≤ phi ∧ phi ≤ theta ∧ theta ≤ Real.pi / 4)

def GerverSofa.PartE.ThirdFourthEquations (A B phi theta : ℝ) : Prop

The last two displayed equations of the DeepMind system.

Equations

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

theorem GerverSofa.PartE.fourthEquation_iff_b_eq_bFromA (A B phi theta : ℝ) : A + Real.pi / 2 - phi - theta - (B - (theta - phi) * (1 + A) / 2 - (theta - phi) ^ 2 / 4) = 0 ↔ B = bFromA A phi theta

The fourth equation is exactly the affine reconstruction formula for B.

theorem GerverSofa.PartE.thirdEquation_iff_mul_denominator_eq_numerator (A B phi theta : ℝ) (hB : B = bFromA A phi theta) : A * Real.cos phi - (Real.sin phi + 1 / 2 - Real.cos phi / 2 + B * Real.sin phi) = 0 ↔ A * angleDenominator phi theta = angleNumerator phi theta

After the fourth equation has reconstructed B, the third equation is exactly A * denominator = numerator.

theorem GerverSofa.PartE.thirdFourthEquations_iff_eliminated (A B phi theta : ℝ) : ThirdFourthEquations A B phi theta ↔ B = bFromA A phi theta ∧ A * angleDenominator phi theta = angleNumerator phi theta

Exact simultaneous elimination statement for equations three and four.

theorem GerverSofa.PartE.physicalAngleDomain_of_physicalDomain {A B phi theta : ℝ} (h : PhysicalDomain (reducedParams A B phi theta)) : PhysicalAngleDomain phi theta

The physical four-variable domain projects to the triangular angle domain.

theorem GerverSofa.PartE.bBase_nonneg_of_physicalAngleDomain {phi theta : ℝ} (h : PhysicalAngleDomain phi theta) : 0 ≤ bBase phi theta

The constant part of the reconstructed B is nonnegative throughout the physical angle triangle.

theorem GerverSofa.PartE.sin_phi_nonneg_of_physicalAngleDomain {phi theta : ℝ} (h : PhysicalAngleDomain phi theta) : 0 ≤ Real.sin phi

The sine of the first switching angle is nonnegative in the physical triangle.

theorem GerverSofa.PartE.cos_phi_pos_of_physicalAngleDomain {phi theta : ℝ} (h : PhysicalAngleDomain phi theta) : 0 < Real.cos phi

The cosine of the first switching angle is strictly positive in the physical triangle.

theorem GerverSofa.PartE.angleDenominator_ne_zero_of_physical_and_equations {A B phi theta : ℝ} (hdom : PhysicalDomain (reducedParams A B phi theta)) (heq : DeepMindEquations A B phi theta) : angleDenominator phi theta ≠ 0

No physical solution of all four equations can hit the apparent zero denominator of the two-angle reconstruction.

theorem GerverSofa.PartE.a_eq_reconstructed_of_physical_and_equations {A B phi theta : ℝ} (hdom : PhysicalDomain (reducedParams A B phi theta)) (heq : DeepMindEquations A B phi theta) : A = reconstructedA phi theta

Every physical four-variable solution has the reconstructed value of A.

theorem GerverSofa.PartE.b_eq_reconstructed_of_physical_and_equations {A B phi theta : ℝ} (hdom : PhysicalDomain (reducedParams A B phi theta)) (heq : DeepMindEquations A B phi theta) : B = reconstructedB phi theta

Every physical four-variable solution has the reconstructed value of B.

def GerverSofa.PartE.TwoAngleEquations (phi theta : ℝ) : Prop

The first two equations after exact reconstruction of A and B.

Equations

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

def GerverSofa.PartE.TwoAngleSpec (phi theta : ℝ) : Prop

Complete two-dimensional specification equivalent to existence of a physical solution with the given two angles.

Equations

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

noncomputable def GerverSofa.PartE.reconstructedParams (phi theta : ℝ) : Reduced.Params

The reconstructed parameters assembled as a reduced-system record.

Equations

• GerverSofa.PartE.reconstructedParams phi theta = GerverSofa.PartE.reducedParams (GerverSofa.PartE.reconstructedA phi theta) (GerverSofa.PartE.reconstructedB phi theta) phi theta

theorem GerverSofa.PartE.deepMindSpec_of_twoAngleSpec {phi theta : ℝ} (h : TwoAngleSpec phi theta) : DeepMindABPhiThetaSpec (reconstructedA phi theta) (reconstructedB phi theta) phi theta

Two-angle data reconstruct a physical solution of all four displayed DeepMind equations.

theorem GerverSofa.PartE.exists_deepMindSpec_iff_twoAngleSpec (phi theta : ℝ) : (∃ (A : ℝ) (B : ℝ), DeepMindABPhiThetaSpec A B phi theta) ↔ TwoAngleSpec phi theta

Exact dimension reduction: for fixed angles, a physical four-variable solution exists if and only if the reconstructed two-angle specification holds.

def GerverSofa.PartE.TwoAngleEnclosureTarget : Prop

The sole mathematical target left after E02. Unlike E01's four-variable target, this quantifies only over the compact triangle of the two angles.

Equations

• GerverSofa.PartE.TwoAngleEnclosureTarget = ∀ (phi theta : ℝ), GerverSofa.PartE.TwoAngleSpec phi theta → GerverSofa.PartE.reconstructedParams phi theta ∈ GerverSofa.Reduced.box

theorem GerverSofa.PartE.globalEnclosureTarget_of_twoAngleEnclosure (hangle : TwoAngleEnclosureTarget) : GlobalEnclosureTarget

A proof of the two-angle enclosure target yields E01's full global enclosure target.

theorem GerverSofa.PartE.deepMindABPhiTheta_existsUnique_of_twoAngleEnclosure (hangle : TwoAngleEnclosureTarget) : ∃! ABphiTheta : ℝ × ℝ × ℝ × ℝ, DeepMindABPhiThetaSpec ABphiTheta.1 ABphiTheta.2.1 ABphiTheta.2.2.1 ABphiTheta.2.2.2

Terminal E02 bridge: the exact DeepMind-shaped uniqueness theorem now requires only the compact two-angle enclosure theorem.

Part E03: division-free two-angle residuals and interval rejection kernel

E02 reduced the four-variable DeepMind system to two angles, but its reconstructed values contain a quotient. Direct interval evaluation of that quotient is unnecessarily singular near the corner where its denominator can vanish.

This module clears the denominator exactly. It proves that, whenever the E02 denominator is nonzero, the two original reconstructed equations are equivalent to two smooth residuals containing only addition, multiplication, sin, cos, and the named constant pi.

The same residuals are encoded as LeanCert expressions. The final theorem is a reusable, executable cell-rejection kernel: if certified interval evaluation of either residual excludes zero on a rational rectangle, no common zero can lie in that rectangle. E03 intentionally does not postulate a global cover; the finite branch-and-bound cover is the next data layer.

noncomputable def GerverSofa.PartE.firstReconstructedResidual (phi theta : ℝ) : ℝ

First reconstructed E02 equation, written as a residual.

Equations

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

noncomputable def GerverSofa.PartE.secondReconstructedResidual (phi theta : ℝ) : ℝ

Second reconstructed E02 equation, written as a residual.

Equations

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

noncomputable def GerverSofa.PartE.scaledB (phi theta : ℝ) : ℝ

Numerator of denominator * reconstructedB, with no division.

Equations

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

noncomputable def GerverSofa.PartE.scaledResidualOne (phi theta : ℝ) : ℝ

Division-free first residual.

Equations

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

noncomputable def GerverSofa.PartE.scaledResidualTwo (phi theta : ℝ) : ℝ

Division-free second residual.

Equations

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

theorem GerverSofa.PartE.denominator_mul_reconstructedB_eq_scaledB (phi theta : ℝ) (hden : angleDenominator phi theta ≠ 0) : angleDenominator phi theta * reconstructedB phi theta = scaledB phi theta

The cleared numerator is exactly denominator * reconstructedB.

theorem GerverSofa.PartE.scaledResidualOne_eq_denominator_mul (phi theta : ℝ) (hden : angleDenominator phi theta ≠ 0) : scaledResidualOne phi theta = angleDenominator phi theta * firstReconstructedResidual phi theta

The first smooth residual is the original residual multiplied by the E02 denominator.

theorem GerverSofa.PartE.scaledResidualTwo_eq_denominator_mul (phi theta : ℝ) (hden : angleDenominator phi theta ≠ 0) : scaledResidualTwo phi theta = angleDenominator phi theta * secondReconstructedResidual phi theta

The second smooth residual is the original residual multiplied by the E02 denominator.

theorem GerverSofa.PartE.twoAngleEquations_iff_reconstructedResiduals_zero (phi theta : ℝ) : TwoAngleEquations phi theta ↔ firstReconstructedResidual phi theta = 0 ∧ secondReconstructedResidual phi theta = 0

E02's two equations are exactly the vanishing of the two ordinary reconstructed residuals.

theorem GerverSofa.PartE.twoAngleEquations_iff_scaledResiduals_zero (phi theta : ℝ) (hden : angleDenominator phi theta ≠ 0) : TwoAngleEquations phi theta ↔ scaledResidualOne phi theta = 0 ∧ scaledResidualTwo phi theta = 0

Exact denominator-clearing equivalence used by the interval layer.

def GerverSofa.PartE.ScaledTwoAngleSpec (phi theta : ℝ) : Prop

The complete E02 specification with only smooth equations in its final conjunct.

Equations

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

theorem GerverSofa.PartE.twoAngleSpec_iff_scaledTwoAngleSpec (phi theta : ℝ) : TwoAngleSpec phi theta ↔ ScaledTwoAngleSpec phi theta

No mathematical information is lost by clearing the denominator.

def GerverSofa.PartE.ScaledResidualEnclosureTarget : Prop

E02's remaining enclosure target, now stated over division-free equations.

Equations

• GerverSofa.PartE.ScaledResidualEnclosureTarget = ∀ (phi theta : ℝ), GerverSofa.PartE.ScaledTwoAngleSpec phi theta → GerverSofa.PartE.reconstructedParams phi theta ∈ GerverSofa.Reduced.box

theorem GerverSofa.PartE.scaledResidualEnclosureTarget_iff_twoAngleEnclosureTarget : ScaledResidualEnclosureTarget ↔ TwoAngleEnclosureTarget

The smooth-residual enclosure target is exactly the E02 target.

LeanCert expression model

def GerverSofa.PartE.scaledResidualExprList : List LeanCert.Core.Expr

LeanCert AST for the two division-free residuals. Variable 0 is phi and variable 1 is theta.

Equations

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

def GerverSofa.PartE.scaledResidualExpr (i : Fin 2) : LeanCert.Core.Expr

Select one of the two scaled residual expressions for the angle system.

Equations

• GerverSofa.PartE.scaledResidualExpr i = GerverSofa.PartE.scaledResidualExprList.getD (↑i) (GerverSofa.PartALeanCert.ec 0)

theorem GerverSofa.PartE.scaledResidualExpr_supported (i : Fin 2) : PartALeanCert.ADConstSupported (scaledResidualExpr i)

Both ASTs belong to LeanCert's fully proved core and AD fragment.

theorem GerverSofa.PartE.scaledResidualExpr_eval_zero (phi theta : ℝ) : LeanCert.Engine.evalFin (scaledResidualExpr 0) ![phi, theta] = scaledResidualOne phi theta

theorem GerverSofa.PartE.scaledResidualExpr_eval_one (phi theta : ℝ) : LeanCert.Engine.evalFin (scaledResidualExpr 1) ![phi, theta] = scaledResidualTwo phi theta

def GerverSofa.PartE.angleIntervalEnv (phiI thetaI : LeanCert.Core.IntervalRat) : LeanCert.Engine.IntervalEnv

Rational interval environment for the two angle variables.

Equations

• GerverSofa.PartE.angleIntervalEnv phiI thetaI 0 = phiI
• GerverSofa.PartE.angleIntervalEnv phiI thetaI 1 = thetaI
• GerverSofa.PartE.angleIntervalEnv phiI thetaI x✝ = default

def GerverSofa.PartE.intervalExcludesZero (I : LeanCert.Core.IntervalRat) : Bool

Executable test that an interval lies strictly on one side of zero.

Equations

• GerverSofa.PartE.intervalExcludesZero I = decide (I.hi < 0 ∨ 0 < I.lo)

theorem GerverSofa.PartE.intervalExcludesZero_sound (I : LeanCert.Core.IntervalRat) (h : intervalExcludesZero I = true) : 0 ∉ I

The executable zero-exclusion test is sound over real interval membership.

Part E04: finite-cover replay foundation

E03 supplied a sound, executable rejection theorem for one rational rectangle in the (phi, theta) plane. This module lifts that kernel to finite lists of rectangles and states the exact two remaining data obligations:

1. a finite rejected cover of the physical angle triangle outside the angle projection of Reduced.box;
2. local reconstruction into Reduced.box inside that angle projection.

Their conjunction yields TwoAngleEnclosureTarget and therefore the exact DeepMind-shaped uniqueness theorem. No cover or local enclosure is assumed as an axiom: both remain ordinary theorem arguments.

The module also replays one nontrivial pilot rectangle near the origin. This checks the complete path from rational cell data through LeanCert interval evaluation to the no-common-zero theorem before the large cover is generated.

def GerverSofa.PartE.scaledResidualKernelInterval (i : Fin 2) (phiI thetaI : LeanCert.Core.IntervalRat) (cfg : LeanCert.Engine.EvalConfig := { }) : LeanCert.Core.IntervalRat

Kernel-reducible interval evaluation for one smooth residual. This uses the already certified project-specialized interval for pi, avoiding the generic named-constant normalization bottleneck in closed decide replays.

Equations

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

theorem GerverSofa.PartE.scaledResidual_mem_kernelInterval (i : Fin 2) (phi theta : ℝ) (phiI thetaI : LeanCert.Core.IntervalRat) (hphi : phi ∈ phiI) (htheta : theta ∈ thetaI) (cfg : LeanCert.Engine.EvalConfig := { }) : (if i = 0 then scaledResidualOne phi theta else scaledResidualTwo phi theta) ∈ scaledResidualKernelInterval i phiI thetaI cfg

Soundness of the kernel-reducible residual evaluator.

structure GerverSofa.PartE.AngleCell : Type

A rational rectangle in the two-angle plane.

• phiI : LeanCert.Core.IntervalRat

  The rational interval for the first switching angle φ.

• thetaI : LeanCert.Core.IntervalRat

  The rational interval for the second switching angle θ.

def GerverSofa.PartE.AngleCell.Contains (cell : AngleCell) (phi theta : ℝ) : Prop

Real point membership in a rational angle cell.

Equations

• cell.Contains phi theta = (phi ∈ cell.phiI ∧ theta ∈ cell.thetaI)

def GerverSofa.PartE.AngleCell.rejected (cell : AngleCell) (cfg : LeanCert.Engine.EvalConfig := { }) : Bool

Executable E03 rejection test for a complete angle cell.

Equations

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

theorem GerverSofa.PartE.AngleCell.no_common_zero_of_rejected (cell : AngleCell) (phi theta : ℝ) (hmem : cell.Contains phi theta) (cfg : LeanCert.Engine.EvalConfig := { }) (hreject : cell.rejected cfg = true) : ¬(scaledResidualOne phi theta = 0 ∧ scaledResidualTwo phi theta = 0)

A cell accepted by the executable checker contains no common zero of the two smooth residuals.

Pilot replay

Part E21F: local two-angle Krawczyk closure repair

The residual-only cover becomes inefficient close to the certified Gerver zero. This module replaces arbitrarily deep subdivision there by a single two-dimensional contraction certificate on a deliberately wider rational box. The wide box contains both the exact projection of Reduced.box and the complete unresolved E19 tail.

The resulting theorem identifies every smooth residual zero in the wide box with the already certified Part A reduced solution. A terminal composition theorem therefore needs interval rejection only outside this wide local box.

Concrete two-dimensional contraction data

def GerverSofa.PartE.localAngleX : Fin 2 → LeanCert.Core.IntervalRat

Local angle box containing the complete unresolved E20 tail and the exact angle projection of Reduced.box. E21F narrows the exploratory E21 box to the region actually required by the recorded E20 extrema.

Equations

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

def GerverSofa.PartE.localAngleCenter : Fin 2 → ℚ

Rational center near the already certified Gerver zero.

Equations

• GerverSofa.PartE.localAngleCenter = ![3917736479 / 100000000000, 681301509383 / 1000000000000]

def GerverSofa.PartE.localAngleY : Matrix (Fin 2) (Fin 2) ℚ

Rational approximation to the inverse Jacobian of the two scaled residuals at localAngleCenter.

Equations

• GerverSofa.PartE.localAngleY = ![![-2886 / 10000, -1481 / 10000], ![6267 / 10000, -27218 / 10000]]

def GerverSofa.PartE.localAngleCfg : LeanCert.Engine.EvalConfig

The default interval-evaluation configuration for local angle certification.

Equations

• GerverSofa.PartE.localAngleCfg = { }

def GerverSofa.PartE.localAngleQ : ℚ

Contraction constant used by the checked local uniqueness theorem.

Equations

• GerverSofa.PartE.localAngleQ = 3 / 10

def GerverSofa.PartE.localAnglePJ : Matrix (Fin 2) (Fin 2) LeanCert.Core.IntervalRat

Enclose the preconditioned Newton derivative on the local two-angle box.

Equations

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

def GerverSofa.PartE.localAngleImage (i : Fin 2) : LeanCert.Core.IntervalRat

Enclose the local Newton image using the certified contraction bound.

Equations

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

theorem GerverSofa.PartE.localAngleQ_nonneg : 0 ≤ localAngleQ

theorem GerverSofa.PartE.localAngleQ_lt_one : localAngleQ < 1

theorem GerverSofa.PartE.localAngleCenter_mem : LeanCert.Engine.FinBoxMem (fun (i : Fin 2) => ↑(localAngleCenter i)) localAngleX

theorem GerverSofa.PartE.localAngle_bound_lt : LeanCert.Engine.intervalMatrixBound localAnglePJ < localAngleQ

theorem GerverSofa.PartE.localAngle_bound_le : LeanCert.Engine.intervalMatrixBound localAnglePJ ≤ localAngleQ

theorem GerverSofa.PartE.localAngle_image_zero_inside : LeanCert.Engine.intervalStrictInside (localAngleImage 0) (localAngleX 0) = true

theorem GerverSofa.PartE.localAngle_image_one_inside : LeanCert.Engine.intervalStrictInside (localAngleImage 1) (localAngleX 1) = true

theorem GerverSofa.PartE.localAngle_images_inside (i : Fin 2) : LeanCert.Engine.intervalStrictInside (localAngleImage i) (localAngleX i) = true

theorem GerverSofa.PartE.localAngle_unique_scaled : ∃! u : Fin 2 → ℝ, LeanCert.Engine.FinBoxMem u localAngleX ∧ LeanCert.Engine.SystemZero scaledResidualExpr u

Kernel-checked existence and uniqueness of a common scaled-residual zero throughout the complete wide local box.

Semantic bridge to named angles and the Part A solution

def GerverSofa.PartE.localAngleCell : AngleCell

The two-angle cell corresponding to the certified local interval box.

Equations

• GerverSofa.PartE.localAngleCell = { phiI := GerverSofa.PartE.localAngleX 0, thetaI := GerverSofa.PartE.localAngleX 1 }

def GerverSofa.PartE.localAngleVector (phi theta : ℝ) : Fin 2 → ℝ

Package the two switching angles as a two-coordinate real vector.

Equations

• GerverSofa.PartE.localAngleVector phi theta = ![phi, theta]

theorem GerverSofa.PartE.localAngleVector_mem_iff (phi theta : ℝ) : LeanCert.Engine.FinBoxMem (localAngleVector phi theta) localAngleX ↔ localAngleCell.Contains phi theta

theorem GerverSofa.PartE.localAngleVector_systemZero_iff (phi theta : ℝ) : LeanCert.Engine.SystemZero scaledResidualExpr (localAngleVector phi theta) ↔ scaledResidualOne phi theta = 0 ∧ scaledResidualTwo phi theta = 0

noncomputable def GerverSofa.PartE.certifiedReducedSolution : Reduced.Params

The reduced parameter tuple selected by the concrete uniqueness certificate.

Equations

• GerverSofa.PartE.certifiedReducedSolution = GerverSofa.PartALeanCert.reducedCertifiedUniqueSolution.solution

theorem GerverSofa.PartE.certifiedReducedSolution_mem : certifiedReducedSolution ∈ Reduced.box

theorem GerverSofa.PartE.certifiedReducedSolution_satisfies : Reduced.Equations certifiedReducedSolution

theorem GerverSofa.PartE.certifiedAngles_mem_localAngleCell : localAngleCell.Contains certifiedReducedSolution.phi certifiedReducedSolution.theta

The Part A solution's angle pair lies strictly inside the wide local box, by exact rational endpoint comparison.

theorem GerverSofa.PartE.certifiedAngles_mem_localAngleX : LeanCert.Engine.FinBoxMem (localAngleVector certifiedReducedSolution.phi certifiedReducedSolution.theta) localAngleX

theorem GerverSofa.PartE.certifiedAngles_systemZero : LeanCert.Engine.SystemZero scaledResidualExpr (localAngleVector certifiedReducedSolution.phi certifiedReducedSolution.theta)

theorem GerverSofa.PartE.reconstructedParams_mem_reducedBox_of_mem_localAngleCell {phi theta : ℝ} (hspec : ScaledTwoAngleSpec phi theta) (hlocal : localAngleCell.Contains phi theta) : reconstructedParams phi theta ∈ Reduced.box

Every smooth physical solution in the wide local cell reconstructs to the already certified Part A solution and hence belongs to Reduced.box.

Terminal composition with rejection only outside the wide box

def GerverSofa.PartE.WideLocalReconstructionEnclosureTarget : Prop

Solutions in the local angle cell reconstruct into the reduced parameter box.

Equations

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

theorem GerverSofa.PartE.wideLocalReconstructionEnclosureTarget : WideLocalReconstructionEnclosureTarget

Machine-readable replay markers consumed by the E21 runner.

Part E22F foundation: adaptive global cover

This module replaces the probe-only upper-wedge files by one kernel-reducible adaptive checker. Starting from the rational square [0, 4/5]^2, it prunes cells which are outside the physical triangle, cells wholly contained in the wide E21 local box, and cells rejected by the certified E03 interval kernel. Every remaining cell is split into four exact rational children. Depth 18 is the depth reached by the final E20 refinement around the Gerver root.

The soundness theorem is independent of the closed computation. E22F compiles the depth-18 Boolean certificate in sixty-four independent depth-15 modules; ParallelAdaptiveGlobalCoverClosure recombines them without recomputation.

def GerverSofa.PartE.angleMid (i : LeanCert.Core.IntervalRat) : ℚ

The rational midpoint of an angle interval.

Equations

• GerverSofa.PartE.angleMid i = (i.lo + i.hi) / 2

def GerverSofa.PartE.intervalLow (i : LeanCert.Core.IntervalRat) : LeanCert.Core.IntervalRat

The closed lower half of a rational interval.

Equations

• GerverSofa.PartE.intervalLow i = { lo := i.lo, hi := GerverSofa.PartE.angleMid i, le := ⋯ }

def GerverSofa.PartE.intervalHigh (i : LeanCert.Core.IntervalRat) : LeanCert.Core.IntervalRat

The closed upper half of a rational interval.

Equations

• GerverSofa.PartE.intervalHigh i = { lo := GerverSofa.PartE.angleMid i, hi := i.hi, le := ⋯ }

def GerverSofa.PartE.childLL (cell : AngleCell) : AngleCell

Bisect both angle intervals and select the lower φ half and lower θ half.

Equations

• GerverSofa.PartE.childLL cell = { phiI := GerverSofa.PartE.intervalLow cell.phiI, thetaI := GerverSofa.PartE.intervalLow cell.thetaI }

def GerverSofa.PartE.childLH (cell : AngleCell) : AngleCell

Bisect both angle intervals and select the lower φ half and upper θ half.

Equations

• GerverSofa.PartE.childLH cell = { phiI := GerverSofa.PartE.intervalLow cell.phiI, thetaI := GerverSofa.PartE.intervalHigh cell.thetaI }

def GerverSofa.PartE.childHL (cell : AngleCell) : AngleCell

Bisect both angle intervals and select the upper φ half and lower θ half.

Equations

• GerverSofa.PartE.childHL cell = { phiI := GerverSofa.PartE.intervalHigh cell.phiI, thetaI := GerverSofa.PartE.intervalLow cell.thetaI }

def GerverSofa.PartE.childHH (cell : AngleCell) : AngleCell

Bisect both angle intervals and select the upper φ half and upper θ half.

Equations

• GerverSofa.PartE.childHH cell = { phiI := GerverSofa.PartE.intervalHigh cell.phiI, thetaI := GerverSofa.PartE.intervalHigh cell.thetaI }

def GerverSofa.PartE.physicallyIrrelevant (cell : AngleCell) : Bool

A rational cell lies strictly above the physical half-plane phi ≤ theta. The strict comparison deliberately keeps all cells touching the diagonal.

Equations

• GerverSofa.PartE.physicallyIrrelevant cell = decide (cell.thetaI.hi < cell.phiI.lo)

def GerverSofa.PartE.cellInsideLocal (cell : AngleCell) : Bool

Every point of the rational cell lies in the wide E21 local box.

Equations

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

def GerverSofa.PartE.adaptiveCoverCheck : ℕ → AngleCell → Bool

Adaptive four-way replay. A node closes when it is irrelevant, local, or rejected. Otherwise all four rational midpoint children must close.

Equations

• One or more equations did not get rendered due to their size.
• GerverSofa.PartE.adaptiveCoverCheck 0 x✝ = if GerverSofa.PartE.physicallyIrrelevant x✝ = true then true else if GerverSofa.PartE.cellInsideLocal x✝ = true then true else x✝.rejected

theorem GerverSofa.PartE.physicallyIrrelevant_no_physical_point (cell : AngleCell) (phi theta : ℝ) (hirr : physicallyIrrelevant cell = true) (hdom : PhysicalAngleDomain phi theta) (hmem : cell.Contains phi theta) : False

theorem GerverSofa.PartE.cellInsideLocal_sound (cell : AngleCell) (phi theta : ℝ) (hlocal : cellInsideLocal cell = true) (hmem : cell.Contains phi theta) : localAngleCell.Contains phi theta

theorem GerverSofa.PartE.contains_some_midpoint_child (cell : AngleCell) (phi theta : ℝ) (hmem : cell.Contains phi theta) : (childLL cell).Contains phi theta ∨ (childLH cell).Contains phi theta ∨ (childHL cell).Contains phi theta ∨ (childHH cell).Contains phi theta

Every real point in a parent cell belongs to at least one of its four closed midpoint children.

theorem GerverSofa.PartE.adaptiveCoverCheck_no_common_zero (depth : ℕ) (cell : AngleCell) (hcheck : adaptiveCoverCheck depth cell = true) (phi theta : ℝ) (hdom : PhysicalAngleDomain phi theta) (hmem : cell.Contains phi theta) (houtside : ¬localAngleCell.Contains phi theta) : ¬(scaledResidualOne phi theta = 0 ∧ scaledResidualTwo phi theta = 0)

Semantic soundness of the adaptive Boolean replay.

def GerverSofa.PartE.globalAngleRoot : AngleCell

Rational root containing the complete physical angle triangle.

Equations

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

theorem GerverSofa.PartE.physicalAngleDomain_mem_globalAngleRoot (phi theta : ℝ) (hdom : PhysicalAngleDomain phi theta) : globalAngleRoot.Contains phi theta

theorem GerverSofa.PartE.adaptiveCoverCheck_succ_of_children (depth : ℕ) (cell : AngleCell) (hLL : adaptiveCoverCheck depth (childLL cell) = true) (hLH : adaptiveCoverCheck depth (childLH cell) = true) (hHL : adaptiveCoverCheck depth (childHL cell) = true) (hHH : adaptiveCoverCheck depth (childHH cell) = true) : adaptiveCoverCheck (depth + 1) cell = true

A parent closes whenever its four children close. This lemma permits the depth-18 computation to be compiled in independent shards without changing the kernel proposition that is certified.

E24 aligned region foundation

Four rational rectangles are aligned exactly with the four sides of the wide E21 local angle cell. Their union covers every point of the global physical angle root that is not in the local cell.

def GerverSofa.PartE.e24PhiBelowRoot : AngleCell

The exclusion root cell below the local φ interval, with φ ≤ 391/10000.

Equations

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

def GerverSofa.PartE.e24PhiAboveRoot : AngleCell

The exclusion root cell above the local φ interval, with 157/4000 ≤ φ.

Equations

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

def GerverSofa.PartE.e24ThetaBelowRoot : AngleCell

The exclusion root cell below the local θ interval, with θ ≤ 68113/100000.

Equations

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

def GerverSofa.PartE.e24ThetaAboveRoot : AngleCell

The exclusion root cell above the local θ interval, with 34069/50000 ≤ θ.

Equations

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

E24 aligned-region semantic closure

This file contains no closed heavy computation. It proves that the four aligned rectangles cover the complement of the E21 local cell inside the physical triangle and turns four Boolean adaptive-cover certificates into the terminal DeepMind-shaped uniqueness theorem.

theorem GerverSofa.PartE.e24AlignedRoots_cover_outside_local (phi theta : ℝ) (hdom : PhysicalAngleDomain phi theta) (houtside : ¬localAngleCell.Contains phi theta) : e24PhiBelowRoot.Contains phi theta ∨ e24PhiAboveRoot.Contains phi theta ∨ e24ThetaBelowRoot.Contains phi theta ∨ e24ThetaAboveRoot.Contains phi theta

theorem GerverSofa.PartE.e24NoCommonZeroOutsideLocal_of_alignedChecks (hPhiBelow : adaptiveCoverCheck 14 e24PhiBelowRoot = true) (hPhiAbove : adaptiveCoverCheck 16 e24PhiAboveRoot = true) (hThetaBelow : adaptiveCoverCheck 18 e24ThetaBelowRoot = true) (hThetaAbove : adaptiveCoverCheck 19 e24ThetaAboveRoot = true) (phi theta : ℝ) (hdom : PhysicalAngleDomain phi theta) (houtside : ¬localAngleCell.Contains phi theta) : ¬(scaledResidualOne phi theta = 0 ∧ scaledResidualTwo phi theta = 0)

theorem GerverSofa.PartE.e24ScaledResidualEnclosureTarget_of_alignedChecks (hPhiBelow : adaptiveCoverCheck 14 e24PhiBelowRoot = true) (hPhiAbove : adaptiveCoverCheck 16 e24PhiAboveRoot = true) (hThetaBelow : adaptiveCoverCheck 18 e24ThetaBelowRoot = true) (hThetaAbove : adaptiveCoverCheck 19 e24ThetaAboveRoot = true) : ScaledResidualEnclosureTarget

theorem GerverSofa.PartE.deepMindABPhiTheta_existsUnique_of_alignedChecks (hPhiBelow : adaptiveCoverCheck 14 e24PhiBelowRoot = true) (hPhiAbove : adaptiveCoverCheck 16 e24PhiAboveRoot = true) (hThetaBelow : adaptiveCoverCheck 18 e24ThetaBelowRoot = true) (hThetaAbove : adaptiveCoverCheck 19 e24ThetaAboveRoot = true) : ∃! ABphiTheta : ℝ × ℝ × ℝ × ℝ, DeepMindABPhiThetaSpec ABphiTheta.1 ABphiTheta.2.1 ABphiTheta.2.2.1 ABphiTheta.2.2.2

E24KC2 proof helpers

The discovery phase is intentionally outside the trusted chain. It only chooses where to stop splitting and which terminal reason to claim.

Every claimed leaf is then checked by the Lean kernel:

• physically irrelevant leaf -> physicallyIrrelevant cell = true;
• local leaf -> cellInsideLocal cell = true;
• interval-rejected leaf -> cell.rejected = true;
• unresolved frontier -> the old adaptive checker, but with remaining depth <= 9.

These lemmas lift a primitive terminal fact to an adaptiveCoverCheck fact at arbitrary remaining depth without asking the kernel to explore the subtree.

theorem GerverSofa.PartE.adaptiveCoverCheck_true_of_physicallyIrrelevant (depth : ℕ) (cell : AngleCell) (h : physicallyIrrelevant cell = true) : adaptiveCoverCheck depth cell = true

theorem GerverSofa.PartE.adaptiveCoverCheck_true_of_rejected (depth : ℕ) (cell : AngleCell) (h : cell.rejected = true) : adaptiveCoverCheck depth cell = true

E24 kernel child certificate: PhiBelow/HL, remaining depth 13.

theorem GerverSofa.PartE.e24PhiBelowKernelHL : adaptiveCoverCheck 13 (childHL e24PhiBelowRoot) = true

Gerver sofa dependency batch

• KernelOnly.PartB.Definitions.
• KernelOnly.PartB.Parameters.
• KernelOnly.PartB.CellSemanticsCore.
• KernelOnly.PartB.Phase1Semantics.
• KernelOnly.PartB.Phase2Semantics.
• KernelOnly.PartB.Phase3Semantics.
• KernelOnly.PartB.Phase4Semantics.
• KernelOnly.PartB.Phase5Semantics.
• KernelOnly.PartB.CellSemantics.
• KernelOnly.PartB.CellCover.
• KernelOnly.PartB.Continuum.

Part B semantic definitions

The numerical layer from Part A is frozen. This file names the certified parameter vector and the two real support functions whose continuum lower bounds are established by the exact cell certificate.

noncomputable def GerverSofa.PartB.params : Romik.Params

The unique direct-system parameter vector certified in Part A.

Equations

• GerverSofa.PartB.params = GerverSofa.Romik.coordEquiv.symm GerverSofa.PartALeanCert.fullRoot

def GerverSofa.PartB.physicalInterval : Set ℝ

The physical parameter interval.

Equations

• GerverSofa.PartB.physicalInterval = Set.Icc 0 (Real.pi / 2)

noncomputable def GerverSofa.PartB.Gu (s t : ℝ) : ℝ

The two global support functions used in the manuscript's grid lemma.

Equations

• GerverSofa.PartB.Gu s t = 1 + GerverSofa.dot (GerverSofa.Romik.path GerverSofa.PartB.params s - GerverSofa.Romik.path GerverSofa.PartB.params t) (GerverSofa.u s)

noncomputable def GerverSofa.PartB.Gv (s t : ℝ) : ℝ

The vertical support slack between two path positions in the frame at s.

Equations

• GerverSofa.PartB.Gv s t = 1 + GerverSofa.dot (GerverSofa.Romik.path GerverSofa.PartB.params s - GerverSofa.Romik.path GerverSofa.PartB.params t) (GerverSofa.v s)

def GerverSofa.PartB.target : ℝ

The real version of the exact rational target.

Equations

• GerverSofa.PartB.target = ↑GerverSofa.PartB.targetQ

noncomputable def GerverSofa.PartB.nodeTime (i : ℕ) : ℝ

Physical mesh node iπ/128.

Equations

• GerverSofa.PartB.nodeTime i = ↑(GerverSofa.PartB.nodeCoeff i) * Real.pi

def GerverSofa.PartB.cellSet (i : Cell) : Set ℝ

Physical closed cell.

Equations

• GerverSofa.PartB.cellSet i = Set.Icc (GerverSofa.PartB.nodeTime ↑i) (GerverSofa.PartB.nodeTime (↑i + 1))

def GerverSofa.PartB.PointContains (z : RatInterval × RatInterval) (p : Point) : Prop

Semantic containment in a planar interval box.

Equations

• GerverSofa.PartB.PointContains z p = (z.1.Contains p.1 ∧ z.2.Contains p.2)

Part B parameter, matching and regularity certificate

Every theorem in this file is a direct consequence of the concrete Part A unique zero. No numerical computation is repeated.

theorem GerverSofa.PartB.params_mem : params ∈ Romik.box

The certified parameter vector lies in the direct Romik box.

theorem GerverSofa.PartB.params_equations : Romik.Equations params

The certified parameter vector satisfies all 22 direct equations.

theorem GerverSofa.PartB.params_switchOrder : Romik.SwitchOrder params

The four physical switches are correctly ordered.

theorem GerverSofa.PartB.match12 : Romik.path1 params params.phi = Romik.path2 params params.phi

Positional matching at φ.

theorem GerverSofa.PartB.match23 : Romik.path2 params params.theta = Romik.path3 params params.theta

Positional matching at θ.

theorem GerverSofa.PartB.match34 : Romik.path3 params (Real.pi / 2 - params.theta) = Romik.path4 params (Real.pi / 2 - params.theta)

Positional matching at π/2-θ.

theorem GerverSofa.PartB.match45 : Romik.path4 params (Real.pi / 2 - params.phi) = Romik.path5 params (Real.pi / 2 - params.phi)

Positional matching at π/2-φ.

theorem GerverSofa.PartB.continuous_path : Continuous (Romik.path params)

Global continuity of the literal five-phase path.

theorem GerverSofa.PartB.continuous_frame : SE2.ContinuousPath (Romik.frame params)

Global continuity of the associated rigid frame.

theorem GerverSofa.PartB.path_zero : Romik.path params 0 = (0, 0)

Exact initial normalization.

theorem GerverSofa.PartB.phi_bounds : 1958868239504182093160893749 / 50000000000000000000000000000 ≤ params.phi ∧ params.phi ≤ 78354729580167283726435751 / 2000000000000000000000000000

Clean exact bounds for the two independent switching angles.

theorem GerverSofa.PartB.theta_bounds : 34065075469136244723692787727 / 50000000000000000000000000000 ≤ params.theta ∧ params.theta ≤ 34065075469136244723692787983 / 50000000000000000000000000000

Core semantic infrastructure for the Part B cell certificate

Hull, time-cell, certified-root-coordinate and trigonometric containment lemmas are isolated here so the five analytic phases can be compiled and diagnosed independently.

Hull and time-cell semantics

theorem GerverSofa.PartB.contains_intervalHull_left {a b : RatInterval} {x : ℝ} (hx : a.Contains x) : (intervalHull a b).Contains x

theorem GerverSofa.PartB.contains_intervalHull_right {a b : RatInterval} {x : ℝ} (hx : b.Contains x) : (intervalHull a b).Contains x

theorem GerverSofa.PartB.pointContains_hull_left {a b : RatInterval × RatInterval} {x : Point} (hx : PointContains a x) : PointContains (pointHull a b) x

theorem GerverSofa.PartB.pointContains_hull_right {a b : RatInterval × RatInterval} {x : Point} (hx : PointContains b x) : PointContains (pointHull a b) x

theorem GerverSofa.PartB.nodeTime_mono {i j : ℕ} (hij : i ≤ j) : nodeTime i ≤ nodeTime j

theorem GerverSofa.PartB.cellTimeInterval_contains_start (i : Cell) : (cellTimeInterval i).Contains (nodeTime ↑i)

theorem GerverSofa.PartB.cellTimeInterval_contains_end (i : Cell) : (cellTimeInterval i).Contains (nodeTime (↑i + 1))

theorem GerverSofa.PartB.cellTimeInterval_contains {i : Cell} {t : ℝ} (ht : t ∈ cellSet i) : (cellTimeInterval i).Contains t

The Part A root is enclosed coordinatewise

theorem GerverSofa.PartB.root_coord_contains (k : Fin 22) : (ExactReplay.getI ExactReplay.fullInputBox ↑k).Contains (PartALeanCert.fullRoot k)

theorem GerverSofa.PartB.k11_contains : (ExactReplay.getI ExactReplay.fullInputBox 0).Contains params.k11

theorem GerverSofa.PartB.k12_contains : (ExactReplay.getI ExactReplay.fullInputBox 1).Contains params.k12

theorem GerverSofa.PartB.k21_contains : (ExactReplay.getI ExactReplay.fullInputBox 2).Contains params.k21

theorem GerverSofa.PartB.k22_contains : (ExactReplay.getI ExactReplay.fullInputBox 3).Contains params.k22

theorem GerverSofa.PartB.k31_contains : (ExactReplay.getI ExactReplay.fullInputBox 4).Contains params.k31

theorem GerverSofa.PartB.k32_contains : (ExactReplay.getI ExactReplay.fullInputBox 5).Contains params.k32

theorem GerverSofa.PartB.k41_contains : (ExactReplay.getI ExactReplay.fullInputBox 6).Contains params.k41

theorem GerverSofa.PartB.k42_contains : (ExactReplay.getI ExactReplay.fullInputBox 7).Contains params.k42

theorem GerverSofa.PartB.k51_contains : (ExactReplay.getI ExactReplay.fullInputBox 8).Contains params.k51

theorem GerverSofa.PartB.k52_contains : (ExactReplay.getI ExactReplay.fullInputBox 9).Contains params.k52

theorem GerverSofa.PartB.a1_contains : (ExactReplay.getI ExactReplay.fullInputBox 10).Contains params.a1

theorem GerverSofa.PartB.a2_contains : (ExactReplay.getI ExactReplay.fullInputBox 11).Contains params.a2

theorem GerverSofa.PartB.b1_contains : (ExactReplay.getI ExactReplay.fullInputBox 12).Contains params.b1

theorem GerverSofa.PartB.b2_contains : (ExactReplay.getI ExactReplay.fullInputBox 13).Contains params.b2

theorem GerverSofa.PartB.c1_contains : (ExactReplay.getI ExactReplay.fullInputBox 14).Contains params.c1

theorem GerverSofa.PartB.c2_contains : (ExactReplay.getI ExactReplay.fullInputBox 15).Contains params.c2

theorem GerverSofa.PartB.d1_contains : (ExactReplay.getI ExactReplay.fullInputBox 16).Contains params.d1

theorem GerverSofa.PartB.d2_contains : (ExactReplay.getI ExactReplay.fullInputBox 17).Contains params.d2

theorem GerverSofa.PartB.e1_contains : (ExactReplay.getI ExactReplay.fullInputBox 18).Contains params.e1

theorem GerverSofa.PartB.e2_contains : (ExactReplay.getI ExactReplay.fullInputBox 19).Contains params.e2

theorem GerverSofa.PartB.point_contains (q : ℚ) : (RatInterval.point q).Contains ↑q

theorem GerverSofa.PartB.trig_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : (ExactReplay.cosineInterval (cellTimeInterval i)).Contains (Real.cos t) ∧ (ExactReplay.sineInterval (cellTimeInterval i)).Contains (Real.sin t)

Semantic enclosure for analytic path phase 1.

theorem GerverSofa.PartB.cellPiece1_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : PointContains (cellPieceInterval 1 i) (Romik.path1 params t)

Semantic enclosure for analytic path phase 2.

theorem GerverSofa.PartB.cellPiece2_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : PointContains (cellPieceInterval 2 i) (Romik.path2 params t)

Semantic enclosure for analytic path phase 3.

theorem GerverSofa.PartB.cellPiece3_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : PointContains (cellPieceInterval 3 i) (Romik.path3 params t)

Semantic enclosure for analytic path phase 4.

theorem GerverSofa.PartB.cellPiece4_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : PointContains (cellPieceInterval 4 i) (Romik.path4 params t)

Semantic enclosure for analytic path phase 5.

theorem GerverSofa.PartB.cellPiece5_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : PointContains (cellPieceInterval 5 i) (Romik.path5 params t)

Assembly of semantic soundness for the Part B cell certificate

The five phase enclosures are independent modules. This file classifies the four switching cells, selects the appropriate phase/hull, and proves semantic soundness of the two product-cell support expressions.

Switches lie in exactly four mesh cells

Every literal path branch is contained in the selected cell hull

theorem GerverSofa.PartB.cellPath_contains {i : Cell} {t : ℝ} (htCell : t ∈ cellSet i) (htPhys : t ∈ physicalInterval) : PointContains (cellPathInterval i) (Romik.path params t)

The interval selected for a cell contains the literal five-phase path at every physical time in that cell.

Semantic soundness of the two product-cell expressions

theorem GerverSofa.PartB.guCell_contains {i j : Cell} {s t : ℝ} (hsCell : s ∈ cellSet i) (htCell : t ∈ cellSet j) (hsPhys : s ∈ physicalInterval) (htPhys : t ∈ physicalInterval) : (guCellInterval i j).Contains (Gu s t)

theorem GerverSofa.PartB.gvCell_contains {i j : Cell} {s t : ℝ} (hsCell : s ∈ cellSet i) (htCell : t ∈ cellSet j) (hsPhys : s ∈ physicalInterval) (htPhys : t ∈ physicalInterval) : (gvCellInterval i j).Contains (Gv s t)

Coverage by the 64 exact mesh cells

theorem GerverSofa.PartB.exists_cell_cover {t : ℝ} (ht : t ∈ physicalInterval) : ∃ (i : Cell), t ∈ cellSet i

Every physical angle belongs to one of the 64 closed cells between the 65 nodes iπ/128.

Exact continuum support margins

The 64×64 cell certificate is now transported to every pair of physical angles. This is the semantic conclusion needed from Part B.

theorem GerverSofa.PartB.Gu_gt_target (s : ℝ) : s ∈ physicalInterval → ∀ t ∈ physicalInterval, target < Gu s t

First global support inequality on the complete square.

theorem GerverSofa.PartB.Gv_gt_target (s : ℝ) : s ∈ physicalInterval → ∀ t ∈ physicalInterval, target < Gv s t

Second global support inequality on the complete square.

theorem GerverSofa.PartB.global_half_plane_margins : (∀ s ∈ Set.Icc 0 (Real.pi / 2), ∀ t ∈ Set.Icc 0 (Real.pi / 2), 171 / 1000 < Gu s t) ∧ ∀ s ∈ Set.Icc 0 (Real.pi / 2), ∀ t ∈ Set.Icc 0 (Real.pi / 2), 171 / 1000 < Gv s t

Manuscript form of the two 0.171 inequalities.