Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.Foundation.Batch002.

Gerver sofa dependency batch

• KernelOnly.LeanCertGerverData.
• KernelOnly.LeanCertNamedConstAD.
• KernelOnly.LeanCertGerverExpr.
• KernelOnly.LeanCertGerverCorrespondence.
• KernelOnly.LeanCertNoDetKrawczyk.
• KernelOnly.LeanCertGerverNumericsCore.

Part A final adapter data

The original Gerver boxes are affinely normalized to [-1,1]^n. If x = m + D u, then the preconditioner is transformed from C to D⁻¹ C. Consequently

I - (D⁻¹ C) (J_F(x) D) = D⁻¹ (I - C J_F(x)) D,

so the old weighted sup-norm contraction becomes the ordinary infinity norm used by LeanCert.

The preconditioner literals below are exact public copies of the frozen rational data already used by ExactReplay. This avoids exposing private helpers during simplification.

def GerverSofa.PartALeanCert.q (n : ℤ) (d : ℕ) : ℚ

Construct an exact rational from an integer numerator and natural denominator.

Equations

• GerverSofa.PartALeanCert.q n d = ↑n / ↑d

def GerverSofa.PartALeanCert.reducedCData : List (List ℚ)

The rational preconditioner table for the four reduced equations.

Equations

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

def GerverSofa.PartALeanCert.fullCData : List (List ℚ)

The rational preconditioner table for the twenty-two full equations.

Equations

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

def GerverSofa.PartALeanCert.listMatrix {n : ℕ} (rows : List (List ℚ)) : Matrix (Fin n) (Fin n) ℚ

Interpret rational row lists as a square matrix, using zero for missing entries.

Equations

• GerverSofa.PartALeanCert.listMatrix rows i j = GerverSofa.ExactReplay.getQ (GerverSofa.ExactReplay.getRow rows ↑i) ↑j

def GerverSofa.PartALeanCert.boxMid (box : List RatInterval) (i : ℕ) : ℚ

The rational midpoint of a selected interval coordinate.

Equations

• GerverSofa.PartALeanCert.boxMid box i = ((GerverSofa.ExactReplay.getI box i).lo + (GerverSofa.ExactReplay.getI box i).hi) / 2

def GerverSofa.PartALeanCert.boxRad (box : List RatInterval) (i : ℕ) : ℚ

Half the width of a selected rational interval coordinate.

Equations

• GerverSofa.PartALeanCert.boxRad box i = ((GerverSofa.ExactReplay.getI box i).hi - (GerverSofa.ExactReplay.getI box i).lo) / 2

def GerverSofa.PartALeanCert.affineFromBox {n : ℕ} (box : List RatInterval) (u : Fin n → ℝ) : Fin n → ℝ

Map normalized coordinates to the given box using its midpoints and radii.

Equations

• GerverSofa.PartALeanCert.affineFromBox box u i = ↑(GerverSofa.PartALeanCert.boxMid box ↑i) + ↑(GerverSofa.PartALeanCert.boxRad box ↑i) * u i

noncomputable def GerverSofa.PartALeanCert.normalizeToBox {n : ℕ} (box : List RatInterval) (x : Fin n → ℝ) : Fin n → ℝ

Subtract each box midpoint and divide by its coordinate radius.

Equations

• GerverSofa.PartALeanCert.normalizeToBox box x i = (x i - ↑(GerverSofa.PartALeanCert.boxMid box ↑i)) / ↑(GerverSofa.PartALeanCert.boxRad box ↑i)

def GerverSofa.PartALeanCert.unitBox {n : ℕ} : Fin n → LeanCert.Core.IntervalRat

The coordinate box with interval [-1, 1] in every dimension.

Equations

• GerverSofa.PartALeanCert.unitBox x✝ = { lo := -1, hi := 1, le := GerverSofa.PartALeanCert.unitBox._proof_1 }

def GerverSofa.PartALeanCert.zeroCenter {n : ℕ} : Fin n → ℚ

The rational origin used as the normalized Newton center.

Equations

• GerverSofa.PartALeanCert.zeroCenter x✝ = 0

def GerverSofa.PartALeanCert.scaledPreconditioner {n : ℕ} (box : List RatInterval) (rows : List (List ℚ)) : Matrix (Fin n) (Fin n) ℚ

Rescale each preconditioner row by the inverse box radius.

Equations

• GerverSofa.PartALeanCert.scaledPreconditioner box rows i j = (GerverSofa.PartALeanCert.boxRad box ↑i)⁻¹ * GerverSofa.PartALeanCert.listMatrix rows i j

def GerverSofa.PartALeanCert.reducedY : Matrix (Fin 4) (Fin 4) ℚ

The preconditioner for the normalized four-dimensional system.

Equations

• GerverSofa.PartALeanCert.reducedY = GerverSofa.PartALeanCert.scaledPreconditioner GerverSofa.ExactReplay.reducedInputBox GerverSofa.PartALeanCert.reducedCData

def GerverSofa.PartALeanCert.fullY : Matrix (Fin 22) (Fin 22) ℚ

The preconditioner for the normalized twenty-two-dimensional system.

Equations

• GerverSofa.PartALeanCert.fullY = GerverSofa.PartALeanCert.scaledPreconditioner GerverSofa.ExactReplay.fullInputBox GerverSofa.PartALeanCert.fullCData

def GerverSofa.PartALeanCert.reducedAffine : (Fin 4 → ℝ) → Fin 4 → ℝ

Map the normalized unit box into the reduced parameter box.

Equations

• GerverSofa.PartALeanCert.reducedAffine = GerverSofa.PartALeanCert.affineFromBox GerverSofa.ExactReplay.reducedInputBox

def GerverSofa.PartALeanCert.fullAffine : (Fin 22 → ℝ) → Fin 22 → ℝ

Map the normalized unit box into the full Romik parameter box.

Equations

• GerverSofa.PartALeanCert.fullAffine = GerverSofa.PartALeanCert.affineFromBox GerverSofa.ExactReplay.fullInputBox

noncomputable def GerverSofa.PartALeanCert.reducedNormalize : (Fin 4 → ℝ) → Fin 4 → ℝ

Convert reduced parameter coordinates to normalized box coordinates.

Equations

• GerverSofa.PartALeanCert.reducedNormalize = GerverSofa.PartALeanCert.normalizeToBox GerverSofa.ExactReplay.reducedInputBox

def GerverSofa.PartALeanCert.qTarget : ℚ

A deliberately generous verified contraction target. The legacy exact bounds are ~5.2e-13 (4D) and ~8.6e-11 (22D), so 1/100 leaves many orders of magnitude of slack while keeping the normalized self-map well inside the unit box.

Equations

• GerverSofa.PartALeanCert.qTarget = 1 / 100

Minimal named-constant extension of LeanCert's AD soundness layer

LeanCert's computable total dual evaluator already evaluates Expr.namedConst c as DualInterval.ofMathConst c, whose derivative component is the singleton interval {0}. Its public ADSupported predicate, however, does not currently include namedConst.

The Gerver systems necessarily contain the exact constant Real.pi. This file adds exactly one missing syntactic case -- differentiable named mathematical constants -- while reusing LeanCert's existing evaluator, interval Jacobian, matrix norm machinery, Newton map, and contraction theorem unchanged.

No interval arithmetic is reimplemented here.

inductive GerverSofa.PartALeanCert.ADConstSupported : LeanCert.Core.Expr → Prop

The LeanCert AD fragment plus named mathematical constants. Every constructor here is everywhere differentiable.

• const (q : ℚ) : ADConstSupported (LeanCert.Core.Expr.const q)
• var (idx : ℕ) : ADConstSupported (LeanCert.Core.Expr.var idx)
• add {a b : LeanCert.Core.Expr} : ADConstSupported a → ADConstSupported b → ADConstSupported (a.add b)
• mul {a b : LeanCert.Core.Expr} : ADConstSupported a → ADConstSupported b → ADConstSupported (a.mul b)
• neg {a : LeanCert.Core.Expr} : ADConstSupported a → ADConstSupported a.neg
• exp {a : LeanCert.Core.Expr} : ADConstSupported a → ADConstSupported a.exp
• sin {a : LeanCert.Core.Expr} : ADConstSupported a → ADConstSupported a.sin
• cos {a : LeanCert.Core.Expr} : ADConstSupported a → ADConstSupported a.cos
• namedConst (c : LeanCert.Core.MathConst) : ADConstSupported (LeanCert.Core.Expr.namedConst c)

def GerverSofa.PartALeanCert.checkADConstSupported : LeanCert.Core.Expr → Bool

Computable recognition of the exact fragment used by the Gerver models.

Equations

• GerverSofa.PartALeanCert.checkADConstSupported (LeanCert.Core.Expr.const q) = true
• GerverSofa.PartALeanCert.checkADConstSupported (LeanCert.Core.Expr.var idx) = true
• GerverSofa.PartALeanCert.checkADConstSupported (LeanCert.Core.Expr.namedConst c) = true
• GerverSofa.PartALeanCert.checkADConstSupported (a.add b) = (GerverSofa.PartALeanCert.checkADConstSupported a && GerverSofa.PartALeanCert.checkADConstSupported b)
• GerverSofa.PartALeanCert.checkADConstSupported (a.mul b) = (GerverSofa.PartALeanCert.checkADConstSupported a && GerverSofa.PartALeanCert.checkADConstSupported b)
• GerverSofa.PartALeanCert.checkADConstSupported a.neg = GerverSofa.PartALeanCert.checkADConstSupported a
• GerverSofa.PartALeanCert.checkADConstSupported a.exp = GerverSofa.PartALeanCert.checkADConstSupported a
• GerverSofa.PartALeanCert.checkADConstSupported a.sin = GerverSofa.PartALeanCert.checkADConstSupported a
• GerverSofa.PartALeanCert.checkADConstSupported a.cos = GerverSofa.PartALeanCert.checkADConstSupported a
• GerverSofa.PartALeanCert.checkADConstSupported x✝ = false

theorem GerverSofa.PartALeanCert.checkADConstSupported_correct {e : LeanCert.Core.Expr} (h : checkADConstSupported e = true) : ADConstSupported e

theorem GerverSofa.PartALeanCert.ADConstSupported.toCore {e : LeanCert.Core.Expr} (h : ADConstSupported e) : LeanCert.Core.ExprSupportedCore e

theorem GerverSofa.PartALeanCert.ADConstSupported.domainValidDual {e : LeanCert.Core.Expr} (h : ADConstSupported e) (ρ : LeanCert.Engine.DualEnv) (cfg : LeanCert.Engine.EvalConfig) : LeanCert.Engine.evalDomainValidDual e ρ cfg

Dual-evaluator domain validity is likewise automatic for this fragment.

Calculus layer

theorem GerverSofa.PartALeanCert.evalFin_differentiable_const {n : ℕ} (e : LeanCert.Core.Expr) (h : ADConstSupported e) : Differentiable ℝ (LeanCert.Engine.evalFin e)

theorem GerverSofa.PartALeanCert.evalAlong_differentiable_const (e : LeanCert.Core.Expr) (h : ADConstSupported e) (ρ : ℕ → ℝ) (idx : ℕ) : Differentiable ℝ (e.evalAlong ρ idx)

theorem GerverSofa.PartALeanCert.evalDualTotalCore_der_correct_idx_const (e : LeanCert.Core.Expr) (h : ADConstSupported e) (ρReal : ℕ → ℝ) (ρInt : LeanCert.Engine.IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (x : ℝ) (hx : x ∈ ρInt idx) (cfg : LeanCert.Engine.EvalConfig) : deriv (e.evalAlong ρReal idx) x ∈ (LeanCert.Internal.AD.evalTotalCore e (LeanCert.Engine.Optimization.mkDualEnvCore ρInt idx) cfg).der

LeanCert's computable total AD derivative theorem, extended by the single missing namedConst case. The computed interval is unchanged.

Krawczyk calculus adapters retaining LeanCert's data path

theorem GerverSofa.PartALeanCert.fderiv_single_eq_deriv_evalAlong_const {n : ℕ} (e : LeanCert.Core.Expr) (h : ADConstSupported e) (x : Fin n → ℝ) (j : Fin n) : (fderiv ℝ (LeanCert.Engine.evalFin e) x) (Pi.single j 1) = deriv (e.evalAlong (LeanCert.Engine.finEnv x) ↑j) (x j)

theorem GerverSofa.PartALeanCert.systemEval_differentiable_const {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) : Differentiable ℝ (LeanCert.Engine.systemEval F)

theorem GerverSofa.PartALeanCert.jacobianAt_apply_const {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) (x : Fin n → ℝ) (i j : Fin n) : LeanCert.Engine.jacobianAt F x i j = deriv ((F i).evalAlong (LeanCert.Engine.finEnv x) ↑j) (x j)

theorem GerverSofa.PartALeanCert.jacobianAt_mem_intervalJacobian_const {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (x : Fin n → ℝ) (hx : LeanCert.Engine.FinBoxMem x X) (cfg : LeanCert.Engine.EvalConfig) (i j : Fin n) : LeanCert.Engine.jacobianAt F x i j ∈ LeanCert.Engine.intervalJacobian F X cfg i j

theorem GerverSofa.PartALeanCert.newtonMap_differentiable_const {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) : Differentiable ℝ (LeanCert.Engine.newtonMap Y F)

theorem GerverSofa.PartALeanCert.newtonMap_fderiv_matrix_const {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) (x : Fin n → ℝ) : LinearMap.toMatrix' ↑(fderiv ℝ (LeanCert.Engine.newtonMap Y F) x) = 1 - Y * LeanCert.Engine.jacobianAt F x

theorem GerverSofa.PartALeanCert.newtonMap_fderiv_norm_le_const {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (x : Fin n → ℝ) (hx : LeanCert.Engine.FinBoxMem x X) (cfg : LeanCert.Engine.EvalConfig) : ‖fderiv ℝ (LeanCert.Engine.newtonMap (Y.map fun (q : ℚ) => ↑q) F) x‖ ≤ ↑(LeanCert.Engine.intervalMatrixBound (LeanCert.Engine.preconditionedJacobian Y (LeanCert.Engine.intervalJacobian F X cfg)))

LeanCert expression models for the normalized Gerver systems

These expressions use LeanCert's differentiable AD fragment plus exact named mathematical constants. LeanCertNamedConstAD supplies the one missing soundness case for namedConst (derivative zero).

@[reducible, inline]

abbrev GerverSofa.PartALeanCert.E : Type

The expression syntax interpreted by the certified interval evaluator.

Equations

• GerverSofa.PartALeanCert.E = LeanCert.Core.Expr

def GerverSofa.PartALeanCert.ec (r : ℚ) : E

A rational constant expression.

Equations

• GerverSofa.PartALeanCert.ec r = LeanCert.Core.Expr.const r

def GerverSofa.PartALeanCert.ev (i : ℕ) : E

An indexed variable expression.

Equations

• GerverSofa.PartALeanCert.ev i = LeanCert.Core.Expr.var i

def GerverSofa.PartALeanCert.eadd (a b : E) : E

Construct the sum of two expressions.

Equations

• GerverSofa.PartALeanCert.eadd a b = LeanCert.Core.Expr.add a b

def GerverSofa.PartALeanCert.eneg (a : E) : E

Construct the negation of an expression.

Equations

• GerverSofa.PartALeanCert.eneg a = LeanCert.Core.Expr.neg a

def GerverSofa.PartALeanCert.esub (a b : E) : E

Construct a difference using addition and negation.

Equations

• GerverSofa.PartALeanCert.esub a b = LeanCert.Core.Expr.add a (LeanCert.Core.Expr.neg b)

def GerverSofa.PartALeanCert.emul (a b : E) : E

Construct the product of two expressions.

Equations

• GerverSofa.PartALeanCert.emul a b = LeanCert.Core.Expr.mul a b

def GerverSofa.PartALeanCert.escale (r : ℚ) (a : E) : E

Multiply an expression by a rational constant.

Equations

• GerverSofa.PartALeanCert.escale r a = (LeanCert.Core.Expr.const r).mul a

def GerverSofa.PartALeanCert.esin (a : E) : E

Apply sine in the expression syntax.

Equations

• GerverSofa.PartALeanCert.esin a = LeanCert.Core.Expr.sin a

def GerverSofa.PartALeanCert.ecos (a : E) : E

Apply cosine in the expression syntax.

Equations

• GerverSofa.PartALeanCert.ecos a = LeanCert.Core.Expr.cos a

def GerverSofa.PartALeanCert.epi : E

The named π constant in the expression syntax.

Equations

• GerverSofa.PartALeanCert.epi = LeanCert.Core.Expr.namedConst LeanCert.Core.MathConst.pi

def GerverSofa.PartALeanCert.scaledVar (box : List RatInterval) (i : ℕ) : E

An expression for a box coordinate in terms of its normalized variable.

Equations

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

Reduced 4D

def GerverSofa.PartALeanCert.reducedExprList : List E

The four reduced equations encoded as evaluator expressions.

Equations

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

def GerverSofa.PartALeanCert.reducedExpr (i : Fin 4) : E

Select an equation from the reduced four-dimensional expression system.

Equations

• GerverSofa.PartALeanCert.reducedExpr i = GerverSofa.PartALeanCert.reducedExprList.getD (↑i) (GerverSofa.PartALeanCert.ec 0)

Direct 22D

def GerverSofa.PartALeanCert.fv (i : ℕ) : E

A full Romik parameter encoded as a normalized variable expression.

Equations

• GerverSofa.PartALeanCert.fv i = GerverSofa.PartALeanCert.scaledVar GerverSofa.ExactReplay.fullInputBox i

def GerverSofa.PartALeanCert.phiE : E

The expression for the first switching angle φ.

Equations

• GerverSofa.PartALeanCert.phiE = GerverSofa.PartALeanCert.fv 20

def GerverSofa.PartALeanCert.thetaE : E

The expression for the second switching angle θ.

Equations

• GerverSofa.PartALeanCert.thetaE = GerverSofa.PartALeanCert.fv 21

def GerverSofa.PartALeanCert.etaE : E

The expression for the reflected angle π/2 - θ.

Equations

• GerverSofa.PartALeanCert.etaE = GerverSofa.PartALeanCert.esub (GerverSofa.PartALeanCert.escale (1 / 2) GerverSofa.PartALeanCert.epi) GerverSofa.PartALeanCert.thetaE

def GerverSofa.PartALeanCert.tauE : E

The expression for the reflected angle π/2 - φ.

Equations

• GerverSofa.PartALeanCert.tauE = GerverSofa.PartALeanCert.esub (GerverSofa.PartALeanCert.escale (1 / 2) GerverSofa.PartALeanCert.epi) GerverSofa.PartALeanCert.phiE

def GerverSofa.PartALeanCert.rotE (t z1 z2 : E) : E × E

Rotate a pair of coordinate expressions by an angle expression.

Equations

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

def GerverSofa.PartALeanCert.pathPieceE (j : ℕ) (t : E) : E × E

Encode a selected closed path branch as two coordinate expressions.

Equations

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

def GerverSofa.PartALeanCert.alphaBetaE (j : ℕ) (t : E) : E × E

Encode the body-frame velocity of a selected path branch.

Equations

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

def GerverSofa.PartALeanCert.pathPrimeE (j : ℕ) (t : E) : E × E

Encode the world-frame derivative of a selected path branch.

Equations

• GerverSofa.PartALeanCert.pathPrimeE j t = GerverSofa.PartALeanCert.rotE t (GerverSofa.PartALeanCert.alphaBetaE j t).1 (GerverSofa.PartALeanCert.alphaBetaE j t).2

def GerverSofa.PartALeanCert.fullExprList : List E

The twenty-two full equations encoded as evaluator expressions.

Equations

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

def GerverSofa.PartALeanCert.fullExpr (i : Fin 22) : E

Select one equation from the full Romik expression system.

Equations

• GerverSofa.PartALeanCert.fullExpr i = GerverSofa.PartALeanCert.fullExprList.getD (↑i) (GerverSofa.PartALeanCert.ec 0)

theorem GerverSofa.PartALeanCert.reducedExpr_supported (i : Fin 4) : ADConstSupported (reducedExpr i)

Purely syntactic support checks for the Gerver expression fragment.

theorem GerverSofa.PartALeanCert.fullExpr_supported (i : Fin 22) : ADConstSupported (fullExpr i)

Gerver Sofa / Kernel Only / Lean Cert Gerver Correspondence

@[simp]

theorem GerverSofa.PartALeanCert.mathConst_pi_toReal : LeanCert.Core.MathConst.pi.toReal = Real.pi

LeanCert's named π has exactly Mathlib's real value.

Reduced semantic correspondence.

theorem GerverSofa.PartALeanCert.reducedExpr_eval_0 (u : Fin 4 → ℝ) : LeanCert.Engine.evalFin (reducedExpr 0) u = Reduced.vectorSystem (reducedAffine u) 0

theorem GerverSofa.PartALeanCert.reducedExpr_eval_1 (u : Fin 4 → ℝ) : LeanCert.Engine.evalFin (reducedExpr 1) u = Reduced.vectorSystem (reducedAffine u) 1

theorem GerverSofa.PartALeanCert.reducedExpr_eval_2 (u : Fin 4 → ℝ) : LeanCert.Engine.evalFin (reducedExpr 2) u = Reduced.vectorSystem (reducedAffine u) 2

theorem GerverSofa.PartALeanCert.reducedExpr_eval_3 (u : Fin 4 → ℝ) : LeanCert.Engine.evalFin (reducedExpr 3) u = Reduced.vectorSystem (reducedAffine u) 3

theorem GerverSofa.PartALeanCert.reduced_systemEval_eq (u : Fin 4 → ℝ) : LeanCert.Engine.systemEval reducedExpr u = Reduced.vectorSystem (reducedAffine u)

Full 22D semantic correspondence through the already proved public fullDualOutput_model_eq. This avoids unfolding the private pathPrime helper.

theorem GerverSofa.PartALeanCert.fullExpr_eval_0 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 0) u = Romik.vectorSystem (fullAffine u) 0

theorem GerverSofa.PartALeanCert.fullExpr_eval_1 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 1) u = Romik.vectorSystem (fullAffine u) 1

theorem GerverSofa.PartALeanCert.fullExpr_eval_2 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 2) u = Romik.vectorSystem (fullAffine u) 2

theorem GerverSofa.PartALeanCert.fullExpr_eval_3 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 3) u = Romik.vectorSystem (fullAffine u) 3

theorem GerverSofa.PartALeanCert.fullExpr_eval_4 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 4) u = Romik.vectorSystem (fullAffine u) 4

theorem GerverSofa.PartALeanCert.fullExpr_eval_5 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 5) u = Romik.vectorSystem (fullAffine u) 5

theorem GerverSofa.PartALeanCert.fullExpr_eval_6 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 6) u = Romik.vectorSystem (fullAffine u) 6

theorem GerverSofa.PartALeanCert.fullExpr_eval_7 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 7) u = Romik.vectorSystem (fullAffine u) 7

theorem GerverSofa.PartALeanCert.fullExpr_eval_8 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 8) u = Romik.vectorSystem (fullAffine u) 8

theorem GerverSofa.PartALeanCert.fullExpr_eval_9 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 9) u = Romik.vectorSystem (fullAffine u) 9

theorem GerverSofa.PartALeanCert.fullExpr_eval_10 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 10) u = Romik.vectorSystem (fullAffine u) 10

theorem GerverSofa.PartALeanCert.fullExpr_eval_11 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 11) u = Romik.vectorSystem (fullAffine u) 11

theorem GerverSofa.PartALeanCert.fullExpr_eval_12 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 12) u = Romik.vectorSystem (fullAffine u) 12

theorem GerverSofa.PartALeanCert.fullExpr_eval_13 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 13) u = Romik.vectorSystem (fullAffine u) 13

theorem GerverSofa.PartALeanCert.fullExpr_eval_14 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 14) u = Romik.vectorSystem (fullAffine u) 14

theorem GerverSofa.PartALeanCert.fullExpr_eval_15 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 15) u = Romik.vectorSystem (fullAffine u) 15

theorem GerverSofa.PartALeanCert.fullExpr_eval_16 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 16) u = Romik.vectorSystem (fullAffine u) 16

theorem GerverSofa.PartALeanCert.fullExpr_eval_17 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 17) u = Romik.vectorSystem (fullAffine u) 17

theorem GerverSofa.PartALeanCert.fullExpr_eval_18 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 18) u = Romik.vectorSystem (fullAffine u) 18

theorem GerverSofa.PartALeanCert.fullExpr_eval_19 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 19) u = Romik.vectorSystem (fullAffine u) 19

theorem GerverSofa.PartALeanCert.fullExpr_eval_20 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 20) u = Romik.vectorSystem (fullAffine u) 20

theorem GerverSofa.PartALeanCert.fullExpr_eval_21 (u : Fin 22 → ℝ) : LeanCert.Engine.evalFin (fullExpr 21) u = Romik.vectorSystem (fullAffine u) 21

theorem GerverSofa.PartALeanCert.full_systemEval_eq (u : Fin 22 → ℝ) : LeanCert.Engine.systemEval fullExpr u = Romik.vectorSystem (fullAffine u)

Box transport

theorem GerverSofa.PartALeanCert.reduced_box_strict (i : Fin 4) : (ExactReplay.getI ExactReplay.reducedInputBox ↑i).lo < (ExactReplay.getI ExactReplay.reducedInputBox ↑i).hi

theorem GerverSofa.PartALeanCert.full_box_strict (i : Fin 22) : (ExactReplay.getI ExactReplay.fullInputBox ↑i).lo < (ExactReplay.getI ExactReplay.fullInputBox ↑i).hi

theorem GerverSofa.PartALeanCert.affine_mem_interval (z : RatInterval) (hz : z.lo < z.hi) (u : ℝ) (hu : -1 ≤ u ∧ u ≤ 1) : z.Contains (↑((z.lo + z.hi) / 2) + ↑((z.hi - z.lo) / 2) * u)

theorem GerverSofa.PartALeanCert.normalize_mem_unit (z : RatInterval) (hz : z.lo < z.hi) (x : ℝ) (hx : z.Contains x) : (x - ↑((z.lo + z.hi) / 2)) / ↑((z.hi - z.lo) / 2) ∈ unitBox 0

theorem GerverSofa.PartALeanCert.affine_normalize_coord (z : RatInterval) (hz : z.lo < z.hi) (x : ℝ) : ↑((z.lo + z.hi) / 2) + ↑((z.hi - z.lo) / 2) * ((x - ↑((z.lo + z.hi) / 2)) / ↑((z.hi - z.lo) / 2)) = x

theorem GerverSofa.PartALeanCert.reducedAffine_mem {u : Fin 4 → ℝ} (hu : LeanCert.Engine.FinBoxMem u unitBox) : reducedAffine u ∈ Reduced.vectorBox

theorem GerverSofa.PartALeanCert.fullAffine_mem {u : Fin 22 → ℝ} (hu : LeanCert.Engine.FinBoxMem u unitBox) : fullAffine u ∈ Romik.vectorBox

theorem GerverSofa.PartALeanCert.reducedNormalize_mem {x : Fin 4 → ℝ} (hx : x ∈ Reduced.vectorBox) : LeanCert.Engine.FinBoxMem (reducedNormalize x) unitBox

theorem GerverSofa.PartALeanCert.reducedAffine_normalize (x : Fin 4 → ℝ) : reducedAffine (reducedNormalize x) = x

Determinant-free checked Krawczyk endgame

For a square system, the usual explicit determinant test on the preconditioner is redundant once ‖I - YJ‖ < 1 is known: at any point in the box, YJ = 1 - T with ‖T‖ < 1, hence YJ is a unit by the Neumann-series theorem. Therefore Y is surjective, hence injective in finite dimension.

This matters computationally in dimension 22 because Mathlib's generic Leibniz determinant is the wrong algorithm for a huge exact rational matrix.

Kernel-reducible finite interval sums

LeanCert's public intervalRatMatVec uses Finset.sum with a local proof-transported AddCommMonoid IntervalRat. That is semantically sound, but closed decide +kernel computations can get stuck reducing the transported typeclass instance.

We keep LeanCert's interval operations and mathematical semantics, but package this one finite sum by structural recursion on Fin n. Mathlib's existing Fin.sum_univ_succ is the semantic bridge to the ordinary real finite sum.

def GerverSofa.PartALeanCert.kernelIntervalFinSum {n : ℕ} : (Fin n → LeanCert.Core.IntervalRat) → LeanCert.Core.IntervalRat

A finite interval sum that reduces by structural recursion, with no AddCommMonoid IntervalRat instance involved in computation.

Equations

• GerverSofa.PartALeanCert.kernelIntervalFinSum x_2 = LeanCert.Core.IntervalRat.singleton 0
• GerverSofa.PartALeanCert.kernelIntervalFinSum f = (f 0).add (GerverSofa.PartALeanCert.kernelIntervalFinSum fun (j : Fin n) => f j.succ)

theorem GerverSofa.PartALeanCert.mem_kernelIntervalFinSum (n : ℕ) (x : Fin n → ℝ) (I : Fin n → LeanCert.Core.IntervalRat) : (∀ (i : Fin n), x i ∈ I i) → ∑ i : Fin n, x i ∈ kernelIntervalFinSum I

Semantic soundness of the kernel-reducible finite interval sum.

def GerverSofa.PartALeanCert.kernelIntervalRatMatVec {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (v : Fin n → LeanCert.Core.IntervalRat) : Fin n → LeanCert.Core.IntervalRat

Kernel-reducible exact interval matrix-vector product.

Equations

• GerverSofa.PartALeanCert.kernelIntervalRatMatVec Y v i = GerverSofa.PartALeanCert.kernelIntervalFinSum fun (j : Fin n) => LeanCert.Core.IntervalRat.scale (Y i j) (v j)

Kernel-reducible point values at the Newton center

LeanCert's ordinary rational evaluator uses sinComputableReduced and cosComputableReduced. Those are mathematically excellent general-purpose routines, but their period-reduction step computes a rational floor. On the closed Gerver certificates that floor can prevent decide +kernel from normalizing an otherwise entirely rational proposition.

For the exact Gerver expression fragment (ADConstSupported) we therefore use a tiny point evaluator that is identical on algebraic operations and named constants, but calls the already-proved unreduced Taylor enclosures sinComputable and cosComputable. These enclosures are globally sound for arbitrary real arguments; argument reduction is an optimization, not a soundness requirement. This keeps the Newton-center calculation purely in kernel-reducible rational arithmetic without changing the mathematical map.

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

A kernel-reducible interval for π, using the exact project interval whose semantic soundness is already proved in TranscendentalSoundness.

The generic LeanCert MathConst.interval route is mathematically sound, but its named-constant machinery does not always normalize far enough for closed decide +kernel comparisons. Reusing the project's already-certified exact rational π endpoints removes only that reduction bottleneck; it does not change the represented real constant or weaken any enclosure.

Equations

• GerverSofa.PartALeanCert.kernelPiInterval = { lo := GerverSofa.ExactReplay.piI.lo, hi := GerverSofa.ExactReplay.piI.hi, le := GerverSofa.PartALeanCert.kernelPiInterval._proof_3 }

theorem GerverSofa.PartALeanCert.real_pi_mem_kernelPiInterval : Real.pi ∈ kernelPiInterval

The true real π lies in the kernel-reducible π interval.

def GerverSofa.PartALeanCert.kernelNamedConstInterval (c : LeanCert.Core.MathConst) : LeanCert.Core.IntervalRat

Named constants for the point evaluator. π takes the specialized kernel-reducible path; every other LeanCert named constant keeps LeanCert's public certified interval unchanged.

Equations

• GerverSofa.PartALeanCert.kernelNamedConstInterval c = if c = LeanCert.Core.MathConst.pi then GerverSofa.PartALeanCert.kernelPiInterval else c.interval

def GerverSofa.PartALeanCert.kernelPointEvalCore (e : LeanCert.Core.Expr) (ρ : LeanCert.Engine.IntervalEnv) (depth : ℕ) : LeanCert.Core.IntervalRat

Point evaluator for the everywhere-defined Gerver expression fragment. Unsupported constructors are deliberately mapped to {0}; the soundness lemma below is only stated for ADConstSupported, whose constructors are all handled explicitly.

Equations

• GerverSofa.PartALeanCert.kernelPointEvalCore (LeanCert.Core.Expr.const q) ρ depth = LeanCert.Core.IntervalRat.singleton q
• GerverSofa.PartALeanCert.kernelPointEvalCore (LeanCert.Core.Expr.var idx) ρ depth = ρ idx
• GerverSofa.PartALeanCert.kernelPointEvalCore (a.add b) ρ depth = (GerverSofa.PartALeanCert.kernelPointEvalCore a ρ depth).add (GerverSofa.PartALeanCert.kernelPointEvalCore b ρ depth)
• GerverSofa.PartALeanCert.kernelPointEvalCore (a.mul b) ρ depth = (GerverSofa.PartALeanCert.kernelPointEvalCore a ρ depth).mul (GerverSofa.PartALeanCert.kernelPointEvalCore b ρ depth)
• GerverSofa.PartALeanCert.kernelPointEvalCore a.neg ρ depth = (GerverSofa.PartALeanCert.kernelPointEvalCore a ρ depth).neg
• GerverSofa.PartALeanCert.kernelPointEvalCore a.exp ρ depth = (GerverSofa.PartALeanCert.kernelPointEvalCore a ρ depth).expComputable depth
• GerverSofa.PartALeanCert.kernelPointEvalCore a.sin ρ depth = (GerverSofa.PartALeanCert.kernelPointEvalCore a ρ depth).sinComputable depth
• GerverSofa.PartALeanCert.kernelPointEvalCore a.cos ρ depth = (GerverSofa.PartALeanCert.kernelPointEvalCore a ρ depth).cosComputable depth
• GerverSofa.PartALeanCert.kernelPointEvalCore (LeanCert.Core.Expr.namedConst c) ρ depth = GerverSofa.PartALeanCert.kernelNamedConstInterval c
• GerverSofa.PartALeanCert.kernelPointEvalCore e ρ depth = LeanCert.Core.IntervalRat.singleton 0

theorem GerverSofa.PartALeanCert.eval_mem_kernelPointEvalCore {e : LeanCert.Core.Expr} (h : ADConstSupported e) (ρReal : ℕ → ℝ) (ρInt : LeanCert.Engine.IntervalEnv) (hmem : LeanCert.Engine.envMem ρReal ρInt) (depth : ℕ) : LeanCert.Core.Expr.eval ρReal e ∈ kernelPointEvalCore e ρInt depth

Soundness of the kernel-reducible point evaluator on exactly the Gerver fragment. In the sine/cosine cases this uses LeanCert's global Taylor correctness theorems directly, so no period-reduction hypothesis is needed.

def GerverSofa.PartALeanCert.kernelCenterTaylorDepth (n : ℕ) : ℕ

Taylor depth used only for the Newton-center point values. The reduced system has coordinates at scale about 10^-15; the 22D system contains substantially thinner coordinates. Depth 26 is the smallest retained value after an exact-rational replay of all 22 normalized Newton-center images that still leaves the direct self-map strictly inside the unit box. It materially reduces kernel rational size compared with depth 27/34 while leaving the Jacobian evaluator and its already-passing certificates untouched.

Equations

• GerverSofa.PartALeanCert.kernelCenterTaylorDepth n = if n ≤ 4 then 20 else 26

def GerverSofa.PartALeanCert.pointEvalIntervalsKernel {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (m : Fin n → ℚ) (_cfg : LeanCert.Engine.EvalConfig := { }) : Fin n → LeanCert.Core.IntervalRat

Point-value enclosures for a square system at a rational center.

Equations

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

theorem GerverSofa.PartALeanCert.systemEval_mem_pointEvalIntervalsKernel_const {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) (m : Fin n → ℚ) (cfg : LeanCert.Engine.EvalConfig) (i : Fin n) : LeanCert.Engine.systemEval F (fun (j : Fin n) => ↑(m j)) i ∈ pointEvalIntervalsKernel F m cfg i

Every real system coordinate at the rational center lies in the kernel-reducible point enclosure.

def GerverSofa.PartALeanCert.kernelNewtonCenterInterval {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig := { }) : Fin n → LeanCert.Core.IntervalRat

Kernel-reducible version of LeanCert's Newton-center enclosure.

Equations

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

theorem GerverSofa.PartALeanCert.newtonMap_center_mem_kernel_const {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (h : ∀ (i : Fin n), ADConstSupported (F i)) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (i : Fin n) : LeanCert.Engine.newtonMap (Y.map fun (q : ℚ) => ↑q) F (fun (j : Fin n) => ↑(m j)) i ∈ kernelNewtonCenterInterval F m Y cfg i

The real Newton center lies in the kernel-reducible enclosure.

def GerverSofa.PartALeanCert.imageEnclosureWithQ {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (q : ℚ) : Fin n → LeanCert.Core.IntervalRat

Same checked self-map enclosure as before, now with a kernel-reducible finite interval sum at the Newton center.

Equations

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

theorem GerverSofa.PartALeanCert.mapsTo_of_bound_and_enclosure {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (hsupp : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (hm : LeanCert.Engine.FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (q : ℚ) (hq0 : 0 ≤ q) (hbound : LeanCert.Engine.intervalMatrixBound (LeanCert.Engine.preconditionedJacobian Y (LeanCert.Engine.intervalJacobian F X cfg)) ≤ q) (hencl : ∀ (i : Fin n), LeanCert.Engine.intervalStrictInside (imageEnclosureWithQ F X m Y cfg q i) (X i) = true) : Set.MapsTo (LeanCert.Engine.newtonMap (Y.map fun (r : ℚ) => ↑r) F) (LeanCert.Engine.finBoxSet X) (LeanCert.Engine.finBoxSet X)

theorem GerverSofa.PartALeanCert.preconditioner_injective_of_bound_lt_one {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (hsupp : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (hm : LeanCert.Engine.FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (hq : LeanCert.Engine.intervalMatrixBound (LeanCert.Engine.preconditionedJacobian Y (LeanCert.Engine.intervalJacobian F X cfg)) < 1) : Function.Injective fun (v : Fin n → ℝ) => (Y.map fun (r : ℚ) => ↑r).mulVec v

theorem GerverSofa.PartALeanCert.fixedPoint_iff_systemZero_of_injective {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (Y : Matrix (Fin n) (Fin n) ℚ) (hinj : Function.Injective fun (v : Fin n → ℝ) => (Y.map fun (r : ℚ) => ↑r).mulVec v) (x : Fin n → ℝ) : LeanCert.Engine.newtonMap (Y.map fun (r : ℚ) => ↑r) F x = x ↔ LeanCert.Engine.SystemZero F x

theorem GerverSofa.PartALeanCert.uniqueSystemZero_of_certified_contraction {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (hsupp : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (hm : LeanCert.Engine.FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (q : ℚ) (hq0 : 0 ≤ q) (hq1 : q < 1) (hbound : LeanCert.Engine.intervalMatrixBound (LeanCert.Engine.preconditionedJacobian Y (LeanCert.Engine.intervalJacobian F X cfg)) ≤ q) (hencl : ∀ (i : Fin n), LeanCert.Engine.intervalStrictInside (imageEnclosureWithQ F X m Y cfg q i) (X i) = true) : ∃! x : Fin n → ℝ, LeanCert.Engine.FinBoxMem x X ∧ LeanCert.Engine.SystemZero F x

Cached Newton-center values for large closed systems

For the direct 22D Gerver certificate, recomputing all 22 transcendental point values inside every image-row proposition creates a very large kernel reduction. The following variant accepts independently checked point-value enclosures. It changes no mathematics: each cached interval is accompanied by a kernel proof that the corresponding real system value lies in it.

def GerverSofa.PartALeanCert.intervalContained (I J : LeanCert.Core.IntervalRat) : Prop

Endpoint inclusion between two rational intervals.

Equations

• GerverSofa.PartALeanCert.intervalContained I J = (J.lo ≤ I.lo ∧ I.hi ≤ J.hi)

theorem GerverSofa.PartALeanCert.mem_of_intervalContained {x : ℝ} {I J : LeanCert.Core.IntervalRat} (hx : x ∈ I) (hIJ : intervalContained I J) : x ∈ J

def GerverSofa.PartALeanCert.kernelNewtonCenterIntervalWithValues {n : ℕ} (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (V : Fin n → LeanCert.Core.IntervalRat) : Fin n → LeanCert.Core.IntervalRat

Newton-center enclosure from externally supplied, proof-carrying point value intervals.

Equations

• GerverSofa.PartALeanCert.kernelNewtonCenterIntervalWithValues m Y V i = (LeanCert.Core.IntervalRat.singleton (m i)).sub (GerverSofa.PartALeanCert.kernelIntervalRatMatVec Y V i)

theorem GerverSofa.PartALeanCert.newtonMap_center_mem_kernel_values {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (V : Fin n → LeanCert.Core.IntervalRat) (hV : ∀ (j : Fin n), LeanCert.Engine.systemEval F (fun (k : Fin n) => ↑(m k)) j ∈ V j) (i : Fin n) : LeanCert.Engine.newtonMap (Y.map fun (q : ℚ) => ↑q) F (fun (j : Fin n) => ↑(m j)) i ∈ kernelNewtonCenterIntervalWithValues m Y V i

def GerverSofa.PartALeanCert.imageEnclosureWithValuesQ {n : ℕ} (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (V : Fin n → LeanCert.Core.IntervalRat) (q : ℚ) : Fin n → LeanCert.Core.IntervalRat

Self-map enclosure built from independently certified center values.

Equations

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

theorem GerverSofa.PartALeanCert.mapsTo_of_bound_and_values_enclosure {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (hsupp : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (hm : LeanCert.Engine.FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (q : ℚ) (hq0 : 0 ≤ q) (hbound : LeanCert.Engine.intervalMatrixBound (LeanCert.Engine.preconditionedJacobian Y (LeanCert.Engine.intervalJacobian F X cfg)) ≤ q) (V : Fin n → LeanCert.Core.IntervalRat) (hV : ∀ (j : Fin n), LeanCert.Engine.systemEval F (fun (k : Fin n) => ↑(m k)) j ∈ V j) (hencl : ∀ (i : Fin n), LeanCert.Engine.intervalStrictInside (imageEnclosureWithValuesQ X m Y V q i) (X i) = true) : Set.MapsTo (LeanCert.Engine.newtonMap (Y.map fun (r : ℚ) => ↑r) F) (LeanCert.Engine.finBoxSet X) (LeanCert.Engine.finBoxSet X)

theorem GerverSofa.PartALeanCert.uniqueSystemZero_of_certified_contraction_values {n : ℕ} (F : Fin n → LeanCert.Core.Expr) (hsupp : ∀ (i : Fin n), ADConstSupported (F i)) (X : Fin n → LeanCert.Core.IntervalRat) (m : Fin n → ℚ) (hm : LeanCert.Engine.FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : LeanCert.Engine.EvalConfig) (q : ℚ) (hq0 : 0 ≤ q) (hq1 : q < 1) (hbound : LeanCert.Engine.intervalMatrixBound (LeanCert.Engine.preconditionedJacobian Y (LeanCert.Engine.intervalJacobian F X cfg)) ≤ q) (V : Fin n → LeanCert.Core.IntervalRat) (hV : ∀ (j : Fin n), LeanCert.Engine.systemEval F (fun (k : Fin n) => ↑(m k)) j ∈ V j) (hencl : ∀ (i : Fin n), LeanCert.Engine.intervalStrictInside (imageEnclosureWithValuesQ X m Y V q i) (X i) = true) : ∃! x : Fin n → ℝ, LeanCert.Engine.FinBoxMem x X ∧ LeanCert.Engine.SystemZero F x

LeanCert Gerver numerical core

Only shared definitions and lightweight list lemmas live here. The expensive 22D kernel checks are split into one Lake module per row.

def GerverSofa.PartALeanCert.cfg : LeanCert.Engine.EvalConfig

The default evaluation configuration used for the numerical certificates.

Equations

• GerverSofa.PartALeanCert.cfg = { }

def GerverSofa.PartALeanCert.reducedPJ : Matrix (Fin 4) (Fin 4) LeanCert.Core.IntervalRat

The interval enclosure of the normalized reduced Newton-map derivative.

Equations

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

def GerverSofa.PartALeanCert.fullPJ : Matrix (Fin 22) (Fin 22) LeanCert.Core.IntervalRat

The interval enclosure of the normalized full Newton-map derivative.

Equations

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

theorem GerverSofa.PartALeanCert.qTarget_pos : 0 < qTarget

theorem GerverSofa.PartALeanCert.qTarget_nonneg : 0 ≤ qTarget

theorem GerverSofa.PartALeanCert.qTarget_lt_one : qTarget < 1

theorem GerverSofa.PartALeanCert.foldl_max_lt {xs : List ℚ} {a q : ℚ} (ha : a < q) (hxs : ∀ x ∈ xs, x < q) : List.foldl max a xs < q

Assemble a bound from independently kernel-checked rows without re-running AD.

theorem GerverSofa.PartALeanCert.matrixBound_lt_of_rows {n : ℕ} (A : Matrix (Fin n) (Fin n) LeanCert.Core.IntervalRat) (q : ℚ) (hq0 : 0 < q) (hrows : ∀ (i : Fin n), LeanCert.Engine.intervalMatrixRowBound A i < q) : LeanCert.Engine.intervalMatrixBound A < q

Proof-carrying cache for the 22 Newton-center residuals

These deliberately simple rational intervals are much wider than the actual point residuals, but still narrow enough after the scaled preconditioner to leave a large self-map margin. Each coordinate is checked independently in a separate module before it is used by the final contraction theorem.

def GerverSofa.PartALeanCert.fullPointCacheList : List LeanCert.Core.IntervalRat

Cached interval evaluations of the full system at the normalized center.

Equations

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

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

Select a cached center evaluation of a full-system equation.

Equations

• GerverSofa.PartALeanCert.fullPointCache i = GerverSofa.PartALeanCert.fullPointCacheList.getD (↑i) (LeanCert.Core.IntervalRat.singleton 0)

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

The full Newton image enclosure computed with cached center evaluations.

Equations

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

def GerverSofa.PartALeanCert.reducedImageQ (i : Fin 4) : LeanCert.Core.IntervalRat

The reduced Newton image enclosure on the normalized unit box.

Equations

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

theorem GerverSofa.PartALeanCert.reduced_center_mem : LeanCert.Engine.FinBoxMem (fun (i : Fin 4) => ↑(zeroCenter i)) unitBox

theorem GerverSofa.PartALeanCert.full_center_mem : LeanCert.Engine.FinBoxMem (fun (i : Fin 22) => ↑(zeroCenter i)) unitBox