Gerver sofa: related certificate and semantic modules

• GerverSofa.Foundation.Batch001.

Gerver sofa dependency batch

• Basic.
• KrawczykSpec.
• RationalInterval.
• CertificateManifest.
• ExactReplay.

Basic planar geometry for the moving-sofa problem

This file fixes the exact hallway convention used by the manuscript. The inner quadrant is open, so contact with an inner wall is allowed.

@[reducible, inline]

abbrev GerverSofa.Point : Type

Cartesian coordinates for the hallway and sofa geometry.

Equations

• GerverSofa.Point = (ℝ × ℝ)

def GerverSofa.horizontalArm : Set Point

Horizontal unit-width arm (-∞,1] × [0,1].

Equations

• GerverSofa.horizontalArm = {p : GerverSofa.Point | p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1}

def GerverSofa.verticalArm : Set Point

Vertical unit-width arm [0,1] × (-∞,1].

Equations

• GerverSofa.verticalArm = {p : GerverSofa.Point | 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ p.2 ≤ 1}

def GerverSofa.outerQuarter : Set Point

Closed outer quarter-plane (-∞,1]².

Equations

• GerverSofa.outerQuarter = {p : GerverSofa.Point | p.1 ≤ 1 ∧ p.2 ≤ 1}

def GerverSofa.innerQuarter : Set Point

Open inner quarter-plane (-∞,0)².

Equations

• GerverSofa.innerQuarter = {p : GerverSofa.Point | p.1 < 0 ∧ p.2 < 0}

def GerverSofa.hallway : Set Point

The standard unit right-angled hallway.

Equations

• GerverSofa.hallway = GerverSofa.horizontalArm ∪ GerverSofa.verticalArm

theorem GerverSofa.hallway_eq_outer_diff_inner : hallway = outerQuarter \ innerQuarter

Quarter-plane presentation of the standard hallway.

@[simp]

theorem GerverSofa.mem_horizontalArm (p : Point) : p ∈ horizontalArm ↔ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1

@[simp]

theorem GerverSofa.mem_verticalArm (p : Point) : p ∈ verticalArm ↔ 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ p.2 ≤ 1

@[simp]

theorem GerverSofa.mem_outerQuarter (p : Point) : p ∈ outerQuarter ↔ p.1 ≤ 1 ∧ p.2 ≤ 1

@[simp]

theorem GerverSofa.mem_innerQuarter (p : Point) : p ∈ innerQuarter ↔ p.1 < 0 ∧ p.2 < 0

Specification boundary for interval/Krawczyk certification

The records below make the logical target explicit. A completed numerical formalisation must construct these records from exact interval operations, Taylor bounds for sin/cos, a certified interval Jacobian and the general Krawczyk theorem. No global axiom is introduced here.

structure GerverSofa.CertifiedUniqueSolution {α : Type u_1} (P : α → Prop) (X : Set α) : Type u_1

A unique solution of a predicate inside an explicit set.

• solution : α

  The certified point satisfying the predicate in the specified domain.

• solution_mem : self.solution ∈ X
• satisfies : P self.solution
• unique_iff (y : α) : y ∈ X → (P y ↔ y = self.solution)

theorem GerverSofa.CertifiedUniqueSolution.unique {α : Type u_1} {P : α → Prop} {X : Set α} (c : CertifiedUniqueSolution P X) (y : α) (hy : y ∈ X) (hP : P y) : y = c.solution

Any other solution in the certified domain equals the recorded solution.

@[reducible, inline]

abbrev GerverSofa.Vec (n : ℕ) : Type

Real coordinate vectors indexed by a finite type.

Equations

• GerverSofa.Vec n = (Fin n → ℝ)

def GerverSofa.CertifiedUniqueZero {n : ℕ} (F : Vec n → Vec n) (X : Set (Vec n)) : Type

A unique zero of a vector-valued function in a set.

Equations

• GerverSofa.CertifiedUniqueZero F X = GerverSofa.CertifiedUniqueSolution (fun (x : GerverSofa.Vec n) => F x = 0) X

Exact rational intervals

This module is intentionally small. It provides the decidable relations used to audit the published output manifest. It does not assert that a particular transcendental expression is enclosed; that analytic soundness is a distinct proof obligation.

structure GerverSofa.RatInterval : Type

Rational endpoints used by exact interval computations; no ordering is assumed.

• lo : ℚ

  Lower endpoint of the interval.

• hi : ℚ

  Upper endpoint of the interval.

def GerverSofa.instReprRatInterval.repr : RatInterval → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GerverSofa.instReprRatInterval : Repr RatInterval

Equations

• GerverSofa.instReprRatInterval = { reprPrec := GerverSofa.instReprRatInterval.repr }

@[instance_reducible]

instance GerverSofa.instDecidableEqRatInterval : DecidableEq RatInterval

Equations

• GerverSofa.instDecidableEqRatInterval = GerverSofa.instDecidableEqRatInterval.decEq

def GerverSofa.instDecidableEqRatInterval.decEq (x✝ x✝¹ : RatInterval) : Decidable (x✝ = x✝¹)

Equations

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

def GerverSofa.RatInterval.strictInsideB (x outer : RatInterval) : Bool

Strict inclusion in the interior of another interval.

Equations

• x.strictInsideB outer = decide (outer.lo < x.lo ∧ x.hi < outer.hi)

def GerverSofa.RatInterval.point (x : ℚ) : RatInterval

Point interval.

Equations

• GerverSofa.RatInterval.point x = { lo := x, hi := x }

def GerverSofa.RatInterval.add (x y : RatInterval) : RatInterval

Exact interval addition.

Equations

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

def GerverSofa.RatInterval.neg (x : RatInterval) : RatInterval

Exact interval negation.

Equations

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

def GerverSofa.RatInterval.sub (x y : RatInterval) : RatInterval

Exact interval subtraction.

Equations

• x.sub y = x.add y.neg

def GerverSofa.RatInterval.mul (x y : RatInterval) : RatInterval

Product hull of two rational intervals.

Equations

• x.mul y = { lo := min (min (x.lo * y.lo) (x.lo * y.hi)) (min (x.hi * y.lo) (x.hi * y.hi)), hi := max (max (x.lo * y.lo) (x.lo * y.hi)) (max (x.hi * y.lo) (x.hi * y.hi)) }

Real semantics

def GerverSofa.RatInterval.Contains (z : RatInterval) (x : ℝ) : Prop

Semantic membership of a real number in a rational interval.

Equations

• z.Contains x = (↑z.lo ≤ x ∧ x ≤ ↑z.hi)

@[simp]

theorem GerverSofa.RatInterval.strictInsideB_eq_true_iff (x outer : RatInterval) : x.strictInsideB outer = true ↔ outer.lo < x.lo ∧ x.hi < outer.hi

@[simp]

theorem GerverSofa.RatInterval.contains_point_iff (q : ℚ) (x : ℝ) : (point q).Contains x ↔ x = ↑q

theorem GerverSofa.RatInterval.contains_add {a b : RatInterval} {x y : ℝ} (hx : a.Contains x) (hy : b.Contains y) : (a.add b).Contains (x + y)

Exact interval addition is sound over the reals.

theorem GerverSofa.RatInterval.contains_neg {a : RatInterval} {x : ℝ} (hx : a.Contains x) : a.neg.Contains (-x)

Exact interval negation is sound over the reals.

theorem GerverSofa.RatInterval.contains_sub {a b : RatInterval} {x y : ℝ} (hx : a.Contains x) (hy : b.Contains y) : (a.sub b).Contains (x - y)

Exact interval subtraction is sound over the reals.

theorem GerverSofa.RatInterval.contains_of_subset {x outer : RatInterval} {r : ℝ} (hsub : outer.lo ≤ x.lo ∧ x.hi ≤ outer.hi) (hr : x.Contains r) : outer.Contains r

Closed interval inclusion transports semantic membership.

Multiplicative soundness

theorem GerverSofa.RatInterval.contains_mul {a b : RatInterval} {x y : ℝ} (hx : a.Contains x) (hy : b.Contains y) : (a.mul b).Contains (x * y)

The four-corner product hull contains every real product of members.

theorem GerverSofa.RatInterval.contains_scale {a : ℚ} {z : RatInterval} {x : ℝ} (hx : z.Contains x) : ((point a).mul z).Contains (↑a * x)

Rational scaling is a special case of sound interval multiplication.

theorem GerverSofa.RatInterval.valid_of_contains {z : RatInterval} {x : ℝ} (hx : z.Contains x) : ↑z.lo ≤ ↑z.hi

Semantic validity follows from the existence of a contained real point.

theorem GerverSofa.RatInterval.contains_of_strictInsideB {x outer : RatInterval} {r : ℝ} (hstrict : x.strictInsideB outer = true) (hr : x.Contains r) : outer.Contains r

A strict Boolean inclusion is, in particular, a closed semantic inclusion.

Exact rational audit of the published certificate manifest

This file contains no floating-point literals. Every value is emitted as an integer numerator and a positive integer denominator from the deterministic Python Fraction replay. kernel reduction therefore checks the strict box inclusions and every published rational margin in the Lean kernel/runtime.

This manifest audit deliberately does not by itself prove the analytic soundness of the sine/cosine enclosures or the Krawczyk existence theorem; those proof obligations are represented separately in KrawczykSpec.lean and GerverCertificate.lean.

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

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

Equations

• GerverSofa.CertificateManifest.naturalFromChunks chunks = List.foldl (fun (n part : ℕ) => n * 10 ^ 35 + part) 0 chunks

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

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

Equations

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

def GerverSofa.CertificateManifest.declaredPi : RatInterval

The frozen rational enclosure of π used by the certificate manifest.

Equations

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

def GerverSofa.CertificateManifest.machinPi : RatInterval

The frozen interval obtained from the manifest’s Machin-formula computation.

Equations

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

def GerverSofa.CertificateManifest.x4 : List RatInterval

The four rational intervals specifying the reduced parameter box.

Equations

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

def GerverSofa.CertificateManifest.z22 : List RatInterval

The twenty-two rational intervals specifying the full Romik parameter box.

Equations

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

def GerverSofa.CertificateManifest.piCheck : Bool

Small kernel-checkable chunks of the frozen rational certificate.

The previous one-shot package asked the kernel to normalize the whole executable replay in one enormous decide +kernel. That is logically sound but can take hours. Here the proof path uses the already frozen rational certificate and checks it in bounded, independent chunks. The expensive executable replay is still retained in ExactReplay.lean as a diagnostic cross-check, but it is not recomputed while building the trusted certificate.

Equations

• GerverSofa.CertificateManifest.piCheck = GerverSofa.CertificateManifest.machinPi.strictInsideB GerverSofa.CertificateManifest.declaredPi

theorem GerverSofa.CertificateManifest.piCheck_eq_true : piCheck = true

Executable exact-rational replay of the 4D and 22D Krawczyk inclusions

This is a direct, floating-point-free transcription of the companion Python algorithm. It computes with ℚ, interval automatic differentiation and the frozen rational preconditioners. The analytic theorem saying that the Taylor intervals enclose the real sin and cos, and the abstract Krawczyk theorem, remain separate proof obligations; the arithmetic replay itself is decidable.

def GerverSofa.ExactReplay.q (n : ℤ) (d : ℕ := 1) : ℚ

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

Equations

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

def GerverSofa.ExactReplay.zeroI : RatInterval

The singleton rational interval at zero.

Equations

• GerverSofa.ExactReplay.zeroI = GerverSofa.RatInterval.point 0

def GerverSofa.ExactReplay.oneI : RatInterval

The singleton rational interval at one.

Equations

• GerverSofa.ExactReplay.oneI = GerverSofa.RatInterval.point 1

def GerverSofa.ExactReplay.scale (a : ℚ) (x : RatInterval) : RatInterval

Multiply an interval by a rational singleton using exact interval arithmetic.

Equations

• GerverSofa.ExactReplay.scale a x = (GerverSofa.RatInterval.point a).mul x

def GerverSofa.ExactReplay.factorialQ (n : ℕ) : ℚ

A factorial interpreted as an exact rational number.

Equations

• GerverSofa.ExactReplay.factorialQ n = ↑n.factorial

def GerverSofa.ExactReplay.signedTerm (k : ℕ) (x : ℚ) (power : ℕ) : ℚ

An alternating Taylor term with the specified power and factorial denominator.

Equations

• GerverSofa.ExactReplay.signedTerm k x power = if k % 2 = 0 then x ^ power / GerverSofa.ExactReplay.factorialQ power else -(x ^ power / GerverSofa.ExactReplay.factorialQ power)

def GerverSofa.ExactReplay.sinPartial (x : ℚ) (terms : ℕ) : ℚ

The finite odd-power Taylor sum for sine at a rational argument.

Equations

• GerverSofa.ExactReplay.sinPartial x terms = ∑ k ∈ Finset.range terms, GerverSofa.ExactReplay.signedTerm k x (2 * k + 1)

def GerverSofa.ExactReplay.cosPartial (x : ℚ) (terms : ℕ) : ℚ

The finite even-power Taylor sum for cosine at a rational argument.

Equations

• GerverSofa.ExactReplay.cosPartial x terms = ∑ k ∈ Finset.range terms, GerverSofa.ExactReplay.signedTerm k x (2 * k)

def GerverSofa.ExactReplay.sinBound (x : ℚ) : RatInterval

The interval between the nineteen- and twenty-term sine Taylor sums.

Equations

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

def GerverSofa.ExactReplay.cosBound (x : ℚ) : RatInterval

The interval between the nineteen- and twenty-term cosine Taylor sums.

Equations

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

def GerverSofa.ExactReplay.piI : RatInterval

The rational π enclosure used for trigonometric argument reduction.

Equations

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

def GerverSofa.ExactReplay.atanPartial (x : ℚ) (terms : ℕ) : ℚ

A finite alternating rational Taylor sum for arctangent.

Equations

• GerverSofa.ExactReplay.atanPartial x terms = ∑ k ∈ Finset.range terms, if k % 2 = 0 then x ^ (2 * k + 1) / ↑(2 * k + 1) else -(x ^ (2 * k + 1) / ↑(2 * k + 1))

def GerverSofa.ExactReplay.atanBound (x : ℚ) (lowTerms highTerms : ℕ) : RatInterval

The interval between two specified arctangent Taylor sums.

Equations

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

def GerverSofa.ExactReplay.machinPi : RatInterval

Evaluate the Machin expression 16 atan(1/5) - 4 atan(1/239) by rational intervals.

Equations

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

def GerverSofa.ExactReplay.floorDecimal (x : ℚ) (digits : ℕ := 60) : ℚ

Exact downward rounding to a fixed number of decimal places.

Equations

• GerverSofa.ExactReplay.floorDecimal x digits = ↑⌊x * 10 ^ digits⌋ / 10 ^ digits

def GerverSofa.ExactReplay.ceilDecimal (x : ℚ) (digits : ℕ := 60) : ℚ

Exact upward rounding to a fixed number of decimal places.

Equations

• GerverSofa.ExactReplay.ceilDecimal x digits = ↑⌈x * 10 ^ digits⌉ / 10 ^ digits

def GerverSofa.ExactReplay.outwardDecimal (z : RatInterval) : RatInterval

The same 60-decimal outward rounding used by the submitted verifier.

Equations

• GerverSofa.ExactReplay.outwardDecimal z = { lo := GerverSofa.ExactReplay.floorDecimal z.lo, hi := GerverSofa.ExactReplay.ceilDecimal z.hi }

def GerverSofa.ExactReplay.sinSmall (x : RatInterval) : RatInterval

Evaluate the small-argument sine enclosure with outward decimal rounding.

Equations

• GerverSofa.ExactReplay.sinSmall x = GerverSofa.ExactReplay.outwardDecimal { lo := (GerverSofa.ExactReplay.sinBound x.lo).lo, hi := (GerverSofa.ExactReplay.sinBound x.hi).hi }

def GerverSofa.ExactReplay.cosSmall (x : RatInterval) : RatInterval

Evaluate the small-argument cosine enclosure with outward decimal rounding.

Equations

• GerverSofa.ExactReplay.cosSmall x = GerverSofa.ExactReplay.outwardDecimal { lo := (GerverSofa.ExactReplay.cosBound x.hi).lo, hi := (GerverSofa.ExactReplay.cosBound x.lo).hi }

def GerverSofa.ExactReplay.physicalClamp (x : RatInterval) : RatInterval

Clamp an interval to the physical angular range used by the Gerver certificate. If x ∈ [0, π/2] and x is enclosed by the input interval, then x is still enclosed after clamping once piI has been proved to contain Real.pi.

Equations

• GerverSofa.ExactReplay.physicalClamp x = { lo := max 0 x.lo, hi := min (GerverSofa.ExactReplay.piI.hi / 2) x.hi }

def GerverSofa.ExactReplay.universalTrigInterval : RatInterval

A fail-closed enclosure used only when an externally supplied interval is too wide for the small-argument Taylor/range-reduction evaluator. Every certified Gerver call remains in one of the two sharp branches below, so this fallback does not alter the frozen replay.

Equations

• GerverSofa.ExactReplay.universalTrigInterval = { lo := -1, hi := 1 }

def GerverSofa.ExactReplay.complementInterval (x : RatInterval) : RatInterval

Complementary interval for the identity sin x = cos (π/2-x) and cos x = sin (π/2-x).

Equations

• GerverSofa.ExactReplay.complementInterval x = { lo := max 0 (GerverSofa.ExactReplay.piI.lo / 2 - x.hi), hi := GerverSofa.ExactReplay.piI.hi / 2 - x.lo }

def GerverSofa.ExactReplay.sinI (x : RatInterval) : RatInterval

Evaluate sine by small-argument bounds and complementary-angle reduction.

Equations

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

def GerverSofa.ExactReplay.cosI (x : RatInterval) : RatInterval

Evaluate cosine by small-argument bounds and complementary-angle reduction.

Equations

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

structure GerverSofa.ExactReplay.D : Type

An interval value together with a list of interval partial derivatives.

• val : RatInterval

  The interval enclosing the scalar value.

• der : List RatInterval

  Interval enclosures for the coordinate partial derivatives.

def GerverSofa.ExactReplay.instReprD.repr : D → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GerverSofa.ExactReplay.instReprD : Repr D

Equations

• GerverSofa.ExactReplay.instReprD = { reprPrec := GerverSofa.ExactReplay.instReprD.repr }

def GerverSofa.ExactReplay.D.const (v : RatInterval) (n : ℕ) : D

A constant interval with zero partial derivatives in every coordinate.

Equations

• GerverSofa.ExactReplay.D.const v n = { val := v, der := List.replicate n GerverSofa.ExactReplay.zeroI }

def GerverSofa.ExactReplay.D.pointConst (v : ℚ) (n : ℕ) : D

A rational singleton with zero partial derivatives.

Equations

• GerverSofa.ExactReplay.D.pointConst v n = GerverSofa.ExactReplay.D.const (GerverSofa.RatInterval.point v) n

def GerverSofa.ExactReplay.D.varD (v : RatInterval) (j n : ℕ) : D

An interval variable with the selected coordinate derivative equal to one.

Equations

• GerverSofa.ExactReplay.D.varD v j n = { val := v, der := List.map (fun (k : ℕ) => GerverSofa.RatInterval.point (if k = j then 1 else 0)) (List.range n) }

def GerverSofa.ExactReplay.D.addD (x y : D) : D

Addition with interval propagation of all coordinate derivatives.

Equations

• x.addD y = { val := x.val.add y.val, der := List.zipWith GerverSofa.RatInterval.add x.der y.der }

def GerverSofa.ExactReplay.D.negD (x : D) : D

Negation with interval propagation of all coordinate derivatives.

Equations

• x.negD = { val := x.val.neg, der := List.map GerverSofa.RatInterval.neg x.der }

def GerverSofa.ExactReplay.D.subD (x y : D) : D

Subtraction with interval propagation of all coordinate derivatives.

Equations

• x.subD y = x.addD y.negD

def GerverSofa.ExactReplay.D.mulD (x y : D) : D

Multiplication with interval propagation of all coordinate derivatives.

Equations

• x.mulD y = { val := x.val.mul y.val, der := List.zipWith (fun (dx dy : GerverSofa.RatInterval) => (dx.mul y.val).add (x.val.mul dy)) x.der y.der }

def GerverSofa.ExactReplay.D.scaleD (a : ℚ) (x : D) : D

Rational scaling with interval propagation of all coordinate derivatives.

Equations

• GerverSofa.ExactReplay.D.scaleD a x = { val := GerverSofa.ExactReplay.scale a x.val, der := List.map (GerverSofa.ExactReplay.scale a) x.der }

def GerverSofa.ExactReplay.D.sinD (x : D) : D

Sine with interval propagation of all coordinate derivatives.

Equations

• x.sinD = { val := GerverSofa.ExactReplay.sinI x.val, der := List.map (GerverSofa.ExactReplay.cosI x.val).mul x.der }

def GerverSofa.ExactReplay.D.cosD (x : D) : D

Cosine with interval propagation of all coordinate derivatives.

Equations

• x.cosD = { val := GerverSofa.ExactReplay.cosI x.val, der := List.map (fun (z : GerverSofa.RatInterval) => ((GerverSofa.ExactReplay.sinI x.val).mul z).neg) x.der }

@[instance_reducible]

instance GerverSofa.ExactReplay.D.instAdd : Add D

Equations

• GerverSofa.ExactReplay.D.instAdd = { add := GerverSofa.ExactReplay.D.addD }

@[instance_reducible]

instance GerverSofa.ExactReplay.D.instNeg : Neg D

Equations

• GerverSofa.ExactReplay.D.instNeg = { neg := GerverSofa.ExactReplay.D.negD }

@[instance_reducible]

instance GerverSofa.ExactReplay.D.instSub : Sub D

Equations

• GerverSofa.ExactReplay.D.instSub = { sub := GerverSofa.ExactReplay.D.subD }

@[instance_reducible]

instance GerverSofa.ExactReplay.D.instMul : Mul D

Equations

• GerverSofa.ExactReplay.D.instMul = { mul := GerverSofa.ExactReplay.D.mulD }

@[instance_reducible]

instance GerverSofa.ExactReplay.D.instHMulRat : HMul ℚ D D

Equations

• GerverSofa.ExactReplay.D.instHMulRat = { hMul := GerverSofa.ExactReplay.D.scaleD }

def GerverSofa.ExactReplay.getI (xs : List RatInterval) (i : ℕ) : RatInterval

Read an interval coordinate, returning the zero interval outside the list.

Equations

• GerverSofa.ExactReplay.getI xs i = xs.getD i GerverSofa.ExactReplay.zeroI

def GerverSofa.ExactReplay.getQ (xs : List ℚ) (i : ℕ) : ℚ

Read a rational coordinate, returning zero outside the list.

Equations

• GerverSofa.ExactReplay.getQ xs i = xs.getD i 0

def GerverSofa.ExactReplay.getRow (m : List (List ℚ)) (i : ℕ) : List ℚ

Read a rational matrix row, returning the empty row outside the list.

Equations

• GerverSofa.ExactReplay.getRow m i = m.getD i []

Reduced 4D system

Direct 22D Romik system

Public proof-carrying view and optional executable cross-check

The full executable Krawczyk/grid replay above is intentionally retained, but normalizing it in one kernel reduction is prohibitively expensive. The trusted proof path therefore consumes the frozen exact-rational certificate emitted by the independent replay and checks that certificate in CertificateManifest. This is the standard proof-carrying-data split: expensive certificate discovery is outside the kernel; small rational certificate verification is inside it.

The executable wrappers prefixed by executable remain available for offline cross-checking and provenance.

def GerverSofa.ExactReplay.declaredPiInterval : RatInterval

The rational interval used internally by the executable replay for Real.pi.

Equations

• GerverSofa.ExactReplay.declaredPiInterval = GerverSofa.ExactReplay.piI

def GerverSofa.ExactReplay.sineInterval (x : RatInterval) : RatInterval

Public wrapper around the executable sine enclosure.

Equations

• GerverSofa.ExactReplay.sineInterval x = GerverSofa.ExactReplay.sinI x

def GerverSofa.ExactReplay.cosineInterval (x : RatInterval) : RatInterval

Public wrapper around the executable cosine enclosure.

Equations

• GerverSofa.ExactReplay.cosineInterval x = GerverSofa.ExactReplay.cosI x

def GerverSofa.ExactReplay.reducedInputBox : List RatInterval

Frozen reduced input box used by the trusted certificate.

Equations

• GerverSofa.ExactReplay.reducedInputBox = GerverSofa.CertificateManifest.x4

def GerverSofa.ExactReplay.fullInputBox : List RatInterval

Frozen direct-system input box used by the trusted certificate.

Equations

• GerverSofa.ExactReplay.fullInputBox = GerverSofa.CertificateManifest.z22