Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartB.Semantics.Batch001.
• GerverSofa.KernelOnly.PartB.Certificates.Batch004.
• GerverSofa.KernelOnly.PartB.Certificates.Batch003.
• GerverSofa.KernelOnly.PartB.Certificates.Batch002.
• GerverSofa.KernelOnly.PartB.Certificates.Batch001.
• GerverSofa.KernelOnly.PartB.Semantics.Batch002.

Gerver sofa dependency batch

• KernelOnly.PartB.Arithmetic.
• KernelOnly.PartB.CellCache.

Part B exact product-cell arithmetic

This module is deliberately independent of the noncomputable Part A root. It contains only exact rational interval data, so all 64 diagnostic and production rows can be kernel-reduced without rebuilding semantic layers.

def GerverSofa.PartB.targetQ : ℚ

Exact target 0.171 used by the continuum theorem.

Equations

• GerverSofa.PartB.targetQ = 171 / 1000

@[reducible, inline]

abbrev GerverSofa.PartB.Cell : Type

The 64 closed mesh cells determined by the 65 nodes iπ/128.

Equations

• GerverSofa.PartB.Cell = Fin 64

def GerverSofa.PartB.nodeCoeff (i : ℕ) : ℚ

Exact rational mesh coefficient.

Equations

• GerverSofa.PartB.nodeCoeff i = ↑i / 128

def GerverSofa.PartB.intervalHull (a b : RatInterval) : RatInterval

Hull of two rational intervals.

Equations

• GerverSofa.PartB.intervalHull a b = { lo := min a.lo b.lo, hi := max a.hi b.hi }

def GerverSofa.PartB.pointHull (a b : RatInterval × RatInterval) : RatInterval × RatInterval

Componentwise hull of two planar interval boxes.

Equations

• GerverSofa.PartB.pointHull a b = (GerverSofa.PartB.intervalHull a.1 b.1, GerverSofa.PartB.intervalHull a.2 b.2)

def GerverSofa.PartB.cellTimeInterval (i : Cell) : RatInterval

Exact interval enclosure of one physical time cell.

Equations

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

def GerverSofa.PartB.cellPieceInterval (j : ℕ) (i : Cell) : RatInterval × RatInterval

Exact interval evaluation of one path phase on one complete mesh cell.

Equations

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

def GerverSofa.PartB.cellPathInterval (i : Cell) : RatInterval × RatInterval

The path enclosure for a cell. Four cells contain a switching angle and therefore take the hull of the two adjacent analytic phases.

Equations

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

def GerverSofa.PartB.guCellInterval (i j : Cell) : RatInterval

Exact interval image of Gu on one product cell.

Equations

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

def GerverSofa.PartB.gvCellInterval (i j : Cell) : RatInterval

Exact interval image of Gv on one product cell.

Equations

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

Shared exact interval evaluations for the product-cell certificates

Each table is checked against the original evaluator by the Lean kernel. Sharing these evaluations avoids repeating the same Taylor computations in every row.

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

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

Equations

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

def GerverSofa.PartB.cachedPath00 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 0, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath01 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 1, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath02 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 2, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath03 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 3, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath04 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 4, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath05 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 5, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath06 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 6, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath07 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 7, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath08 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 8, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath09 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 9, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath10 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 10, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath11 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 11, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath12 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 12, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath13 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 13, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath14 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 14, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath15 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 15, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath16 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 16, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath17 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 17, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath18 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 18, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath19 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 19, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath20 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 20, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath21 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 21, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath22 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 22, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath23 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 23, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath24 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 24, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath25 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 25, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath26 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 26, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath27 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 27, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath28 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 28, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath29 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 29, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath30 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 30, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath31 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 31, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath32 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 32, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath33 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 33, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath34 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 34, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath35 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 35, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath36 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 36, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath37 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 37, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath38 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 38, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath39 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 39, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath40 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 40, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath41 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 41, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath42 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 42, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath43 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 43, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath44 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 44, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath45 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 45, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath46 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 46, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath47 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 47, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath48 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 48, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath49 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 49, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath50 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 50, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath51 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 51, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath52 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 52, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath53 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 53, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath54 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 54, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath55 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 55, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath56 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 56, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath57 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 57, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath58 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 58, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath59 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 59, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath60 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 60, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath61 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 61, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath62 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 62, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath63 : RatInterval × RatInterval

The exact cached path-coordinate pair for cell 63, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedPath (i : Cell) : RatInterval × RatInterval

The exact cached path-coordinate pair for the selected angle cell.

Equations

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

def GerverSofa.PartB.cachedCosine00 : RatInterval

The exact cached cosine interval for cell 0, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine01 : RatInterval

The exact cached cosine interval for cell 1, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine02 : RatInterval

The exact cached cosine interval for cell 2, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine03 : RatInterval

The exact cached cosine interval for cell 3, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine04 : RatInterval

The exact cached cosine interval for cell 4, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine05 : RatInterval

The exact cached cosine interval for cell 5, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine06 : RatInterval

The exact cached cosine interval for cell 6, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine07 : RatInterval

The exact cached cosine interval for cell 7, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine08 : RatInterval

The exact cached cosine interval for cell 8, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine09 : RatInterval

The exact cached cosine interval for cell 9, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine10 : RatInterval

The exact cached cosine interval for cell 10, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine11 : RatInterval

The exact cached cosine interval for cell 11, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine12 : RatInterval

The exact cached cosine interval for cell 12, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine13 : RatInterval

The exact cached cosine interval for cell 13, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine14 : RatInterval

The exact cached cosine interval for cell 14, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine15 : RatInterval

The exact cached cosine interval for cell 15, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine16 : RatInterval

The exact cached cosine interval for cell 16, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine17 : RatInterval

The exact cached cosine interval for cell 17, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine18 : RatInterval

The exact cached cosine interval for cell 18, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine19 : RatInterval

The exact cached cosine interval for cell 19, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine20 : RatInterval

The exact cached cosine interval for cell 20, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine21 : RatInterval

The exact cached cosine interval for cell 21, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine22 : RatInterval

The exact cached cosine interval for cell 22, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine23 : RatInterval

The exact cached cosine interval for cell 23, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine24 : RatInterval

The exact cached cosine interval for cell 24, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine25 : RatInterval

The exact cached cosine interval for cell 25, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine26 : RatInterval

The exact cached cosine interval for cell 26, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine27 : RatInterval

The exact cached cosine interval for cell 27, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine28 : RatInterval

The exact cached cosine interval for cell 28, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine29 : RatInterval

The exact cached cosine interval for cell 29, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine30 : RatInterval

The exact cached cosine interval for cell 30, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine31 : RatInterval

The exact cached cosine interval for cell 31, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine32 : RatInterval

The exact cached cosine interval for cell 32, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine33 : RatInterval

The exact cached cosine interval for cell 33, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine34 : RatInterval

The exact cached cosine interval for cell 34, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine35 : RatInterval

The exact cached cosine interval for cell 35, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine36 : RatInterval

The exact cached cosine interval for cell 36, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine37 : RatInterval

The exact cached cosine interval for cell 37, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine38 : RatInterval

The exact cached cosine interval for cell 38, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine39 : RatInterval

The exact cached cosine interval for cell 39, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine40 : RatInterval

The exact cached cosine interval for cell 40, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine41 : RatInterval

The exact cached cosine interval for cell 41, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine42 : RatInterval

The exact cached cosine interval for cell 42, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine43 : RatInterval

The exact cached cosine interval for cell 43, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine44 : RatInterval

The exact cached cosine interval for cell 44, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine45 : RatInterval

The exact cached cosine interval for cell 45, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine46 : RatInterval

The exact cached cosine interval for cell 46, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine47 : RatInterval

The exact cached cosine interval for cell 47, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine48 : RatInterval

The exact cached cosine interval for cell 48, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine49 : RatInterval

The exact cached cosine interval for cell 49, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine50 : RatInterval

The exact cached cosine interval for cell 50, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine51 : RatInterval

The exact cached cosine interval for cell 51, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine52 : RatInterval

The exact cached cosine interval for cell 52, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine53 : RatInterval

The exact cached cosine interval for cell 53, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine54 : RatInterval

The exact cached cosine interval for cell 54, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine55 : RatInterval

The exact cached cosine interval for cell 55, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine56 : RatInterval

The exact cached cosine interval for cell 56, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine57 : RatInterval

The exact cached cosine interval for cell 57, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine58 : RatInterval

The exact cached cosine interval for cell 58, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine59 : RatInterval

The exact cached cosine interval for cell 59, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine60 : RatInterval

The exact cached cosine interval for cell 60, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine61 : RatInterval

The exact cached cosine interval for cell 61, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine62 : RatInterval

The exact cached cosine interval for cell 62, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine63 : RatInterval

The exact cached cosine interval for cell 63, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedCosine (i : Cell) : RatInterval

The exact cached cosine interval for the selected angle cell.

Equations

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

def GerverSofa.PartB.cachedSine00 : RatInterval

The exact cached sine interval for cell 0, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine01 : RatInterval

The exact cached sine interval for cell 1, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine02 : RatInterval

The exact cached sine interval for cell 2, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine03 : RatInterval

The exact cached sine interval for cell 3, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine04 : RatInterval

The exact cached sine interval for cell 4, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine05 : RatInterval

The exact cached sine interval for cell 5, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine06 : RatInterval

The exact cached sine interval for cell 6, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine07 : RatInterval

The exact cached sine interval for cell 7, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine08 : RatInterval

The exact cached sine interval for cell 8, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine09 : RatInterval

The exact cached sine interval for cell 9, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine10 : RatInterval

The exact cached sine interval for cell 10, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine11 : RatInterval

The exact cached sine interval for cell 11, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine12 : RatInterval

The exact cached sine interval for cell 12, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine13 : RatInterval

The exact cached sine interval for cell 13, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine14 : RatInterval

The exact cached sine interval for cell 14, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine15 : RatInterval

The exact cached sine interval for cell 15, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine16 : RatInterval

The exact cached sine interval for cell 16, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine17 : RatInterval

The exact cached sine interval for cell 17, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine18 : RatInterval

The exact cached sine interval for cell 18, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine19 : RatInterval

The exact cached sine interval for cell 19, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine20 : RatInterval

The exact cached sine interval for cell 20, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine21 : RatInterval

The exact cached sine interval for cell 21, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine22 : RatInterval

The exact cached sine interval for cell 22, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine23 : RatInterval

The exact cached sine interval for cell 23, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine24 : RatInterval

The exact cached sine interval for cell 24, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine25 : RatInterval

The exact cached sine interval for cell 25, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine26 : RatInterval

The exact cached sine interval for cell 26, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine27 : RatInterval

The exact cached sine interval for cell 27, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine28 : RatInterval

The exact cached sine interval for cell 28, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine29 : RatInterval

The exact cached sine interval for cell 29, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine30 : RatInterval

The exact cached sine interval for cell 30, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine31 : RatInterval

The exact cached sine interval for cell 31, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine32 : RatInterval

The exact cached sine interval for cell 32, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine33 : RatInterval

The exact cached sine interval for cell 33, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine34 : RatInterval

The exact cached sine interval for cell 34, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine35 : RatInterval

The exact cached sine interval for cell 35, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine36 : RatInterval

The exact cached sine interval for cell 36, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine37 : RatInterval

The exact cached sine interval for cell 37, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine38 : RatInterval

The exact cached sine interval for cell 38, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine39 : RatInterval

The exact cached sine interval for cell 39, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine40 : RatInterval

The exact cached sine interval for cell 40, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine41 : RatInterval

The exact cached sine interval for cell 41, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine42 : RatInterval

The exact cached sine interval for cell 42, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine43 : RatInterval

The exact cached sine interval for cell 43, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine44 : RatInterval

The exact cached sine interval for cell 44, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine45 : RatInterval

The exact cached sine interval for cell 45, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine46 : RatInterval

The exact cached sine interval for cell 46, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine47 : RatInterval

The exact cached sine interval for cell 47, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine48 : RatInterval

The exact cached sine interval for cell 48, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine49 : RatInterval

The exact cached sine interval for cell 49, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine50 : RatInterval

The exact cached sine interval for cell 50, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine51 : RatInterval

The exact cached sine interval for cell 51, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine52 : RatInterval

The exact cached sine interval for cell 52, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine53 : RatInterval

The exact cached sine interval for cell 53, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine54 : RatInterval

The exact cached sine interval for cell 54, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine55 : RatInterval

The exact cached sine interval for cell 55, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine56 : RatInterval

The exact cached sine interval for cell 56, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine57 : RatInterval

The exact cached sine interval for cell 57, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine58 : RatInterval

The exact cached sine interval for cell 58, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine59 : RatInterval

The exact cached sine interval for cell 59, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine60 : RatInterval

The exact cached sine interval for cell 60, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine61 : RatInterval

The exact cached sine interval for cell 61, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine62 : RatInterval

The exact cached sine interval for cell 62, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine63 : RatInterval

The exact cached sine interval for cell 63, sharing kernel reduction.

Equations

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

def GerverSofa.PartB.cachedSine (i : Cell) : RatInterval

The exact cached sine interval for the selected angle cell.

Equations

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

theorem GerverSofa.PartB.cachedPath_eq (i : Cell) : cellPathInterval i = cachedPath i

theorem GerverSofa.PartB.cachedCosine_eq (i : Cell) : ExactReplay.cosineInterval (cellTimeInterval i) = cachedCosine i

theorem GerverSofa.PartB.cachedSine_eq (i : Cell) : ExactReplay.sineInterval (cellTimeInterval i) = cachedSine i

Gerver sofa dependency batch

• KernelOnly.PartB.CellRows.Row48.
• KernelOnly.PartB.CellRows.Row49.
• KernelOnly.PartB.CellRows.Row50.
• KernelOnly.PartB.CellRows.Row51.
• KernelOnly.PartB.CellRows.Row52.
• KernelOnly.PartB.CellRows.Row53.
• KernelOnly.PartB.CellRows.Row54.
• KernelOnly.PartB.CellRows.Row55.
• KernelOnly.PartB.CellRows.Row56.
• KernelOnly.PartB.CellRows.Row57.
• KernelOnly.PartB.CellRows.Row58.
• KernelOnly.PartB.CellRows.Row59.
• KernelOnly.PartB.CellRows.Row60.
• KernelOnly.PartB.CellRows.Row61.
• KernelOnly.PartB.CellRows.Row62.
• KernelOnly.PartB.CellRows.Row63.

Independent exact product-cell lower bounds for row 48. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_48 (j : Cell) : targetQ < (guCellInterval 48 j).lo ∧ targetQ < (gvCellInterval 48 j).lo

Independent exact product-cell lower bounds for row 49. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_49 (j : Cell) : targetQ < (guCellInterval 49 j).lo ∧ targetQ < (gvCellInterval 49 j).lo

Independent exact product-cell lower bounds for row 50. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_50 (j : Cell) : targetQ < (guCellInterval 50 j).lo ∧ targetQ < (gvCellInterval 50 j).lo

Independent exact product-cell lower bounds for row 51. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_51 (j : Cell) : targetQ < (guCellInterval 51 j).lo ∧ targetQ < (gvCellInterval 51 j).lo

Independent exact product-cell lower bounds for row 52. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_52 (j : Cell) : targetQ < (guCellInterval 52 j).lo ∧ targetQ < (gvCellInterval 52 j).lo

Independent exact product-cell lower bounds for row 53. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_53 (j : Cell) : targetQ < (guCellInterval 53 j).lo ∧ targetQ < (gvCellInterval 53 j).lo

Independent exact product-cell lower bounds for row 54. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_54 (j : Cell) : targetQ < (guCellInterval 54 j).lo ∧ targetQ < (gvCellInterval 54 j).lo

Independent exact product-cell lower bounds for row 55. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_55 (j : Cell) : targetQ < (guCellInterval 55 j).lo ∧ targetQ < (gvCellInterval 55 j).lo

Independent exact product-cell lower bounds for row 56. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_56 (j : Cell) : targetQ < (guCellInterval 56 j).lo ∧ targetQ < (gvCellInterval 56 j).lo

Independent exact product-cell lower bounds for row 57. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_57 (j : Cell) : targetQ < (guCellInterval 57 j).lo ∧ targetQ < (gvCellInterval 57 j).lo

Independent exact product-cell lower bounds for row 58. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_58 (j : Cell) : targetQ < (guCellInterval 58 j).lo ∧ targetQ < (gvCellInterval 58 j).lo

Independent exact product-cell lower bounds for row 59. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_59 (j : Cell) : targetQ < (guCellInterval 59 j).lo ∧ targetQ < (gvCellInterval 59 j).lo

Independent exact product-cell lower bounds for row 60. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_60 (j : Cell) : targetQ < (guCellInterval 60 j).lo ∧ targetQ < (gvCellInterval 60 j).lo

Independent exact product-cell lower bounds for row 61. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_61 (j : Cell) : targetQ < (guCellInterval 61 j).lo ∧ targetQ < (gvCellInterval 61 j).lo

Independent exact product-cell lower bounds for row 62. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_62 (j : Cell) : targetQ < (guCellInterval 62 j).lo ∧ targetQ < (gvCellInterval 62 j).lo

Independent exact product-cell lower bounds for row 63. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_63 (j : Cell) : targetQ < (guCellInterval 63 j).lo ∧ targetQ < (gvCellInterval 63 j).lo

Gerver sofa dependency batch

• KernelOnly.PartB.CellRows.Row32.
• KernelOnly.PartB.CellRows.Row33.
• KernelOnly.PartB.CellRows.Row34.
• KernelOnly.PartB.CellRows.Row35.
• KernelOnly.PartB.CellRows.Row36.
• KernelOnly.PartB.CellRows.Row37.
• KernelOnly.PartB.CellRows.Row38.
• KernelOnly.PartB.CellRows.Row39.
• KernelOnly.PartB.CellRows.Row40.
• KernelOnly.PartB.CellRows.Row41.
• KernelOnly.PartB.CellRows.Row42.
• KernelOnly.PartB.CellRows.Row43.
• KernelOnly.PartB.CellRows.Row44.
• KernelOnly.PartB.CellRows.Row45.
• KernelOnly.PartB.CellRows.Row46.
• KernelOnly.PartB.CellRows.Row47.

Independent exact product-cell lower bounds for row 32. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_32 (j : Cell) : targetQ < (guCellInterval 32 j).lo ∧ targetQ < (gvCellInterval 32 j).lo

Independent exact product-cell lower bounds for row 33. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_33 (j : Cell) : targetQ < (guCellInterval 33 j).lo ∧ targetQ < (gvCellInterval 33 j).lo

Independent exact product-cell lower bounds for row 34. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_34 (j : Cell) : targetQ < (guCellInterval 34 j).lo ∧ targetQ < (gvCellInterval 34 j).lo

Independent exact product-cell lower bounds for row 35. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_35 (j : Cell) : targetQ < (guCellInterval 35 j).lo ∧ targetQ < (gvCellInterval 35 j).lo

Independent exact product-cell lower bounds for row 36. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_36 (j : Cell) : targetQ < (guCellInterval 36 j).lo ∧ targetQ < (gvCellInterval 36 j).lo

Independent exact product-cell lower bounds for row 37. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_37 (j : Cell) : targetQ < (guCellInterval 37 j).lo ∧ targetQ < (gvCellInterval 37 j).lo

Independent exact product-cell lower bounds for row 38. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_38 (j : Cell) : targetQ < (guCellInterval 38 j).lo ∧ targetQ < (gvCellInterval 38 j).lo

Independent exact product-cell lower bounds for row 39. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_39 (j : Cell) : targetQ < (guCellInterval 39 j).lo ∧ targetQ < (gvCellInterval 39 j).lo

Independent exact product-cell lower bounds for row 40. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_40 (j : Cell) : targetQ < (guCellInterval 40 j).lo ∧ targetQ < (gvCellInterval 40 j).lo

Independent exact product-cell lower bounds for row 41. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_41 (j : Cell) : targetQ < (guCellInterval 41 j).lo ∧ targetQ < (gvCellInterval 41 j).lo

Independent exact product-cell lower bounds for row 42. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_42 (j : Cell) : targetQ < (guCellInterval 42 j).lo ∧ targetQ < (gvCellInterval 42 j).lo

Independent exact product-cell lower bounds for row 43. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_43 (j : Cell) : targetQ < (guCellInterval 43 j).lo ∧ targetQ < (gvCellInterval 43 j).lo

Independent exact product-cell lower bounds for row 44. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_44 (j : Cell) : targetQ < (guCellInterval 44 j).lo ∧ targetQ < (gvCellInterval 44 j).lo

Independent exact product-cell lower bounds for row 45. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_45 (j : Cell) : targetQ < (guCellInterval 45 j).lo ∧ targetQ < (gvCellInterval 45 j).lo

Independent exact product-cell lower bounds for row 46. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_46 (j : Cell) : targetQ < (guCellInterval 46 j).lo ∧ targetQ < (gvCellInterval 46 j).lo

Independent exact product-cell lower bounds for row 47. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_47 (j : Cell) : targetQ < (guCellInterval 47 j).lo ∧ targetQ < (gvCellInterval 47 j).lo

Gerver sofa dependency batch

• KernelOnly.PartB.CellRows.Row16.
• KernelOnly.PartB.CellRows.Row17.
• KernelOnly.PartB.CellRows.Row18.
• KernelOnly.PartB.CellRows.Row19.
• KernelOnly.PartB.CellRows.Row20.
• KernelOnly.PartB.CellRows.Row21.
• KernelOnly.PartB.CellRows.Row22.
• KernelOnly.PartB.CellRows.Row23.
• KernelOnly.PartB.CellRows.Row24.
• KernelOnly.PartB.CellRows.Row25.
• KernelOnly.PartB.CellRows.Row26.
• KernelOnly.PartB.CellRows.Row27.
• KernelOnly.PartB.CellRows.Row28.
• KernelOnly.PartB.CellRows.Row29.
• KernelOnly.PartB.CellRows.Row30.
• KernelOnly.PartB.CellRows.Row31.

Independent exact product-cell lower bounds for row 16. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_16 (j : Cell) : targetQ < (guCellInterval 16 j).lo ∧ targetQ < (gvCellInterval 16 j).lo

Independent exact product-cell lower bounds for row 17. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_17 (j : Cell) : targetQ < (guCellInterval 17 j).lo ∧ targetQ < (gvCellInterval 17 j).lo

Independent exact product-cell lower bounds for row 18. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_18 (j : Cell) : targetQ < (guCellInterval 18 j).lo ∧ targetQ < (gvCellInterval 18 j).lo

Independent exact product-cell lower bounds for row 19. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_19 (j : Cell) : targetQ < (guCellInterval 19 j).lo ∧ targetQ < (gvCellInterval 19 j).lo

Independent exact product-cell lower bounds for row 20. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_20 (j : Cell) : targetQ < (guCellInterval 20 j).lo ∧ targetQ < (gvCellInterval 20 j).lo

Independent exact product-cell lower bounds for row 21. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_21 (j : Cell) : targetQ < (guCellInterval 21 j).lo ∧ targetQ < (gvCellInterval 21 j).lo

Independent exact product-cell lower bounds for row 22. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_22 (j : Cell) : targetQ < (guCellInterval 22 j).lo ∧ targetQ < (gvCellInterval 22 j).lo

Independent exact product-cell lower bounds for row 23. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_23 (j : Cell) : targetQ < (guCellInterval 23 j).lo ∧ targetQ < (gvCellInterval 23 j).lo

Independent exact product-cell lower bounds for row 24. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_24 (j : Cell) : targetQ < (guCellInterval 24 j).lo ∧ targetQ < (gvCellInterval 24 j).lo

Independent exact product-cell lower bounds for row 25. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_25 (j : Cell) : targetQ < (guCellInterval 25 j).lo ∧ targetQ < (gvCellInterval 25 j).lo

Independent exact product-cell lower bounds for row 26. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_26 (j : Cell) : targetQ < (guCellInterval 26 j).lo ∧ targetQ < (gvCellInterval 26 j).lo

Independent exact product-cell lower bounds for row 27. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_27 (j : Cell) : targetQ < (guCellInterval 27 j).lo ∧ targetQ < (gvCellInterval 27 j).lo

Independent exact product-cell lower bounds for row 28. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_28 (j : Cell) : targetQ < (guCellInterval 28 j).lo ∧ targetQ < (gvCellInterval 28 j).lo

Independent exact product-cell lower bounds for row 29. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_29 (j : Cell) : targetQ < (guCellInterval 29 j).lo ∧ targetQ < (gvCellInterval 29 j).lo

Independent exact product-cell lower bounds for row 30. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_30 (j : Cell) : targetQ < (guCellInterval 30 j).lo ∧ targetQ < (gvCellInterval 30 j).lo

Independent exact product-cell lower bounds for row 31. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_31 (j : Cell) : targetQ < (guCellInterval 31 j).lo ∧ targetQ < (gvCellInterval 31 j).lo

Gerver sofa dependency batch

• KernelOnly.PartB.CellRows.Row00.
• KernelOnly.PartB.CellRows.Row01.
• KernelOnly.PartB.CellRows.Row02.
• KernelOnly.PartB.CellRows.Row03.
• KernelOnly.PartB.CellRows.Row04.
• KernelOnly.PartB.CellRows.Row05.
• KernelOnly.PartB.CellRows.Row06.
• KernelOnly.PartB.CellRows.Row07.
• KernelOnly.PartB.CellRows.Row08.
• KernelOnly.PartB.CellRows.Row09.
• KernelOnly.PartB.CellRows.Row10.
• KernelOnly.PartB.CellRows.Row11.
• KernelOnly.PartB.CellRows.Row12.
• KernelOnly.PartB.CellRows.Row13.
• KernelOnly.PartB.CellRows.Row14.
• KernelOnly.PartB.CellRows.Row15.

Independent exact product-cell lower bounds for row 00. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_00 (j : Cell) : targetQ < (guCellInterval 0 j).lo ∧ targetQ < (gvCellInterval 0 j).lo

Independent exact product-cell lower bounds for row 01. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_01 (j : Cell) : targetQ < (guCellInterval 1 j).lo ∧ targetQ < (gvCellInterval 1 j).lo

Independent exact product-cell lower bounds for row 02. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_02 (j : Cell) : targetQ < (guCellInterval 2 j).lo ∧ targetQ < (gvCellInterval 2 j).lo

Independent exact product-cell lower bounds for row 03. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_03 (j : Cell) : targetQ < (guCellInterval 3 j).lo ∧ targetQ < (gvCellInterval 3 j).lo

Independent exact product-cell lower bounds for row 04. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_04 (j : Cell) : targetQ < (guCellInterval 4 j).lo ∧ targetQ < (gvCellInterval 4 j).lo

Independent exact product-cell lower bounds for row 05. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_05 (j : Cell) : targetQ < (guCellInterval 5 j).lo ∧ targetQ < (gvCellInterval 5 j).lo

Independent exact product-cell lower bounds for row 06. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_06 (j : Cell) : targetQ < (guCellInterval 6 j).lo ∧ targetQ < (gvCellInterval 6 j).lo

Independent exact product-cell lower bounds for row 07. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_07 (j : Cell) : targetQ < (guCellInterval 7 j).lo ∧ targetQ < (gvCellInterval 7 j).lo

Independent exact product-cell lower bounds for row 08. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_08 (j : Cell) : targetQ < (guCellInterval 8 j).lo ∧ targetQ < (gvCellInterval 8 j).lo

Independent exact product-cell lower bounds for row 09. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_09 (j : Cell) : targetQ < (guCellInterval 9 j).lo ∧ targetQ < (gvCellInterval 9 j).lo

Independent exact product-cell lower bounds for row 10. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_10 (j : Cell) : targetQ < (guCellInterval 10 j).lo ∧ targetQ < (gvCellInterval 10 j).lo

Independent exact product-cell lower bounds for row 11. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_11 (j : Cell) : targetQ < (guCellInterval 11 j).lo ∧ targetQ < (gvCellInterval 11 j).lo

Independent exact product-cell lower bounds for row 12. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_12 (j : Cell) : targetQ < (guCellInterval 12 j).lo ∧ targetQ < (gvCellInterval 12 j).lo

Independent exact product-cell lower bounds for row 13. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_13 (j : Cell) : targetQ < (guCellInterval 13 j).lo ∧ targetQ < (gvCellInterval 13 j).lo

Independent exact product-cell lower bounds for row 14. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_14 (j : Cell) : targetQ < (guCellInterval 14 j).lo ∧ targetQ < (gvCellInterval 14 j).lo

Independent exact product-cell lower bounds for row 15. Build all 64 row modules sequentially before the final Part B assembly.

theorem GerverSofa.PartB.cell_row_15 (j : Cell) : targetQ < (guCellInterval 15 j).lo ∧ targetQ < (gvCellInterval 15 j).lo

Gerver sofa dependency batch

• KernelOnly.PartB.AllRows.

Assembly of the 64 independently kernel-checked product-cell rows.

theorem GerverSofa.PartB.all_cell_lower (i j : Cell) : targetQ < (guCellInterval i j).lo ∧ targetQ < (gvCellInterval i j).lo