Gerver sofa: related certificate and semantic modules

• GerverSofa.Foundation.Batch002.
• GerverSofa.KernelOnly.Foundation.Batch001.
• GerverSofa.KernelOnly.PartF.Semantics.Batch001.

Gerver sofa dependency batch

• SE2.
• SupportingHallway.
• Systems.
• Boxes.
• Geometry.

Orientation-preserving rigid motions of the plane

An element is represented by (c,s,tₓ,tᵧ) with c²+s²=1. Its linear part is the rotation matrix [[c,-s],[s,c]], hence every value is an element of SE(2) and not an arbitrary affine equivalence.

structure GerverSofa.SE2 : Type

An orientation-preserving planar rigid motion represented by rotation and translation.

• c : ℝ

  The cosine coefficient of the rotation.

• s : ℝ

  The sine coefficient of the rotation.

• tx : ℝ

  The horizontal translation component.

• ty : ℝ

  The vertical translation component.

• unit : self.c * self.c + self.s * self.s = 1

def GerverSofa.SE2.act (g : SE2) (p : Point) : Point

Action of an orientation-preserving rigid motion on the plane.

Equations

• g.act p = (g.c * p.1 - g.s * p.2 + g.tx, g.s * p.1 + g.c * p.2 + g.ty)

def GerverSofa.SE2.one : SE2

Identity element.

Equations

• GerverSofa.SE2.one = { c := 1, s := 0, tx := 0, ty := 0, unit := GerverSofa.SE2.one._proof_1 }

def GerverSofa.SE2.inv (g : SE2) : SE2

Inverse orientation-preserving rigid motion.

Equations

• g.inv = { c := g.c, s := -g.s, tx := -(g.c * g.tx + g.s * g.ty), ty := g.s * g.tx - g.c * g.ty, unit := ⋯ }

@[simp]

theorem GerverSofa.SE2.one_act (p : Point) : one.act p = p

@[simp]

theorem GerverSofa.SE2.inv_act_act (g : SE2) (p : Point) : g.inv.act (g.act p) = p

@[simp]

theorem GerverSofa.SE2.act_inv_act (g : SE2) (p : Point) : g.act (g.inv.act p) = p

def GerverSofa.SE2.ContinuousPath (g : ℝ → SE2) : Prop

Componentwise continuity is the topology-free representation of a path in SE(2) used by the formal moving-sofa definition.

Equations

• GerverSofa.SE2.ContinuousPath g = ((Continuous fun (t : ℝ) => (g t).c) ∧ (Continuous fun (t : ℝ) => (g t).s) ∧ (Continuous fun (t : ℝ) => (g t).tx) ∧ Continuous fun (t : ℝ) => (g t).ty)

theorem GerverSofa.SE2.continuousPath_inv {g : ℝ → SE2} (hg : ContinuousPath g) : ContinuousPath fun (t : ℝ) => (g t).inv

Inversion preserves continuous SE(2) paths.

Supporting hallway and inverse motion

def GerverSofa.supportingHallway (frame : SE2) : Set Point

World-frame hallway obtained from the standard hallway by frame.

Equations

• GerverSofa.supportingHallway frame = frame.act '' GerverSofa.hallway

theorem GerverSofa.mem_supportingHallway_iff (frame : SE2) (q : Point) : q ∈ supportingHallway frame ↔ frame.inv.act q ∈ hallway

Membership in a supporting hallway is equivalent to standard-hallway membership after applying the inverse frame.

theorem GerverSofa.inv_image_subset_hallway_of_subset_supporting (frame : SE2) (S : Set Point) (hS : S ⊆ supportingHallway frame) : frame.inv.act '' S ⊆ hallway

Set-level version of mem_supportingHallway_iff.

The concrete reduced and 22-dimensional Romik systems

These are direct Lean transcriptions of equations (F1)--(F4) and of the independent equations (27)--(39), (41), (43) used by the companion verifier.

structure GerverSofa.Reduced.Params : Type

The four real parameters of the reduced Gerver equations.

• a : ℝ

  The first scalar parameter in the reduced equations.

• b : ℝ

  The second scalar parameter in the reduced equations.

• phi : ℝ

  The first switching angle.

• theta : ℝ

  The second switching angle.

noncomputable def GerverSofa.Reduced.system (p : Params) : Fin 4 → ℝ

Four-dimensional reduced switching system.

Equations

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

def GerverSofa.Reduced.Equations (p : Params) : Prop

The proposition that all four reduced equations vanish.

Equations

• GerverSofa.Reduced.Equations p = (GerverSofa.Reduced.system p = 0)

structure GerverSofa.Romik.Params : Type

Translation, phase, and switching-angle parameters of the five Romik branches.

• k11 : ℝ

  Horizontal translation coefficient for phase 1.

• k12 : ℝ

  Vertical translation coefficient for phase 1.

• k21 : ℝ

  Horizontal translation coefficient for phase 2.

• k22 : ℝ

  Vertical translation coefficient for phase 2.

• k31 : ℝ

  Horizontal translation coefficient for phase 3.

• k32 : ℝ

  Vertical translation coefficient for phase 3.

• k41 : ℝ

  Horizontal translation coefficient for phase 4.

• k42 : ℝ

  Vertical translation coefficient for phase 4.

• k51 : ℝ

  Horizontal translation coefficient for phase 5.

• k52 : ℝ

  Vertical translation coefficient for phase 5.

• a1 : ℝ

  Coefficient 1 in the phase 1 closed formula.

• a2 : ℝ

  Coefficient 2 in the phase 1 closed formula.

• b1 : ℝ

  Coefficient 1 in the phase 2 closed formula.

• b2 : ℝ

  Coefficient 2 in the phase 2 closed formula.

• c1 : ℝ

  Coefficient 1 in the phase 3 closed formula.

• c2 : ℝ

  Coefficient 2 in the phase 3 closed formula.

• d1 : ℝ

  Coefficient 1 in the phase 4 closed formula.

• d2 : ℝ

  Coefficient 2 in the phase 4 closed formula.

• e1 : ℝ

  Coefficient 1 in the phase 5 closed formula.

• e2 : ℝ

  Coefficient 2 in the phase 5 closed formula.

• phi : ℝ

  First switching angle.

• theta : ℝ

  Second switching angle.

noncomputable def GerverSofa.Romik.rot (t : ℝ) (z : Point) : Point

Rotation of a body-frame vector into the world frame.

Equations

• GerverSofa.Romik.rot t z = (Real.cos t * z.1 - Real.sin t * z.2, Real.sin t * z.1 + Real.cos t * z.2)

def GerverSofa.Romik.addK (r : Point) (kx ky : ℝ) : Point

Translate a point by the two specified coordinate offsets.

Equations

• GerverSofa.Romik.addK r kx ky = (r.1 + kx, r.2 + ky)

noncomputable def GerverSofa.Romik.path1 (p : Params) (t : ℝ) : Point

Phase 1 of the five-phase Gerver path.

Equations

• GerverSofa.Romik.path1 p t = GerverSofa.Romik.addK (GerverSofa.Romik.rot t (p.a1 * Real.cos t + p.a2 * Real.sin t - 1, -p.a2 * Real.cos t + p.a1 * Real.sin t - 1 / 2)) p.k11 p.k12

noncomputable def GerverSofa.Romik.path2 (p : Params) (t : ℝ) : Point

Phase 2 of the five-phase Gerver path.

Equations

• GerverSofa.Romik.path2 p t = GerverSofa.Romik.addK (GerverSofa.Romik.rot t (-(1 / 4) * t * t + p.b1 * t + p.b2, 1 / 2 * t - p.b1 - 1)) p.k21 p.k22

noncomputable def GerverSofa.Romik.path3 (p : Params) (t : ℝ) : Point

Phase 3 of the five-phase Gerver path.

Equations

• GerverSofa.Romik.path3 p t = GerverSofa.Romik.addK (GerverSofa.Romik.rot t (p.c1 - t, p.c2 + t)) p.k31 p.k32

noncomputable def GerverSofa.Romik.path4 (p : Params) (t : ℝ) : Point

Phase 4 of the five-phase Gerver path.

Equations

• GerverSofa.Romik.path4 p t = GerverSofa.Romik.addK (GerverSofa.Romik.rot t (-(1 / 2) * t + p.d1 - 1, -(1 / 4) * t * t + p.d1 * t + p.d2)) p.k41 p.k42

noncomputable def GerverSofa.Romik.path5 (p : Params) (t : ℝ) : Point

Phase 5 of the five-phase Gerver path.

Equations

• GerverSofa.Romik.path5 p t = GerverSofa.Romik.addK (GerverSofa.Romik.rot t (p.e1 * Real.cos t + p.e2 * Real.sin t - 1 / 2, -p.e2 * Real.cos t + p.e1 * Real.sin t - 1)) p.k51 p.k52

noncomputable def GerverSofa.Romik.alphaBeta1 (p : Params) (t : ℝ) : Point

Body-frame derivative coefficients (alpha,beta) on phase 1.

Equations

• GerverSofa.Romik.alphaBeta1 p t = (-2 * p.a1 * Real.sin t + 2 * p.a2 * Real.cos t + 1 / 2, 2 * p.a1 * Real.cos t + 2 * p.a2 * Real.sin t - 1)

noncomputable def GerverSofa.Romik.alphaBeta2 (p : Params) (t : ℝ) : Point

Body-frame velocity coordinates for phase 2.

Equations

• GerverSofa.Romik.alphaBeta2 p t = (1 + 2 * p.b1 - t, -(1 / 4) * t * t + p.b1 * t + p.b2 + 1 / 2)

def GerverSofa.Romik.alphaBeta3 (p : Params) (t : ℝ) : Point

Body-frame velocity coordinates for phase 3.

Equations

• GerverSofa.Romik.alphaBeta3 p t = (-1 - p.c2 - t, 1 + p.c1 - t)

noncomputable def GerverSofa.Romik.alphaBeta4 (p : Params) (t : ℝ) : Point

Body-frame velocity coordinates for phase 4.

Equations

• GerverSofa.Romik.alphaBeta4 p t = (1 / 4 * t * t - p.d1 * t - p.d2 - 1 / 2, 2 * p.d1 - 1 - t)

noncomputable def GerverSofa.Romik.alphaBeta5 (p : Params) (t : ℝ) : Point

Body-frame velocity coordinates for phase 5.

Equations

• GerverSofa.Romik.alphaBeta5 p t = (1 - 2 * p.e1 * Real.sin t + 2 * p.e2 * Real.cos t, 2 * p.e1 * Real.cos t + 2 * p.e2 * Real.sin t - 1 / 2)

noncomputable def GerverSofa.Romik.pathPrimeFromAB (t : ℝ) (ab : Point) : Point

Rotate body-frame velocity coordinates into the world frame.

Equations

• GerverSofa.Romik.pathPrimeFromAB t ab = GerverSofa.Romik.rot t ab

noncomputable def GerverSofa.Romik.pathPrime1 (p : Params) (t : ℝ) : Point

World-frame velocity formula for phase 1.

Equations

• GerverSofa.Romik.pathPrime1 p t = GerverSofa.Romik.pathPrimeFromAB t (GerverSofa.Romik.alphaBeta1 p t)

noncomputable def GerverSofa.Romik.pathPrime2 (p : Params) (t : ℝ) : Point

World-frame velocity formula for phase 2.

Equations

• GerverSofa.Romik.pathPrime2 p t = GerverSofa.Romik.pathPrimeFromAB t (GerverSofa.Romik.alphaBeta2 p t)

noncomputable def GerverSofa.Romik.pathPrime3 (p : Params) (t : ℝ) : Point

World-frame velocity formula for phase 3.

Equations

• GerverSofa.Romik.pathPrime3 p t = GerverSofa.Romik.pathPrimeFromAB t (GerverSofa.Romik.alphaBeta3 p t)

noncomputable def GerverSofa.Romik.system (p : Params) : Fin 22 → ℝ

Romik's 22 independent scalar equations.

Equations

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

def GerverSofa.Romik.Equations (p : Params) : Prop

The proposition that all 22 independent equations vanish.

Equations

• GerverSofa.Romik.Equations p = (GerverSofa.Romik.system p = 0)

noncomputable def GerverSofa.Romik.path (p : Params) (t : ℝ) : Point

The physical five-phase path on [0,π/2]. At a switching angle either adjacent formula may be chosen; the certified matching equations prove they coincide.

Equations

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

noncomputable def GerverSofa.Romik.angle (u : ℝ) : ℝ

Linear normalization from unit time to physical rotation angle.

Equations

• GerverSofa.Romik.angle u = u * (Real.pi / 2)

noncomputable def GerverSofa.Romik.frame (p : Params) (u : ℝ) : SE2

Standard-to-world frame q ↦ x(t)+R_t q for normalized time.

Equations

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

@[simp]

theorem GerverSofa.Romik.angle_zero : angle 0 = 0

@[simp]

theorem GerverSofa.Romik.angle_one : angle 1 = Real.pi / 2

theorem GerverSofa.Romik.continuous_angle : Continuous angle

The normalized physical angle depends continuously on time.

theorem GerverSofa.Romik.continuousPath_frame_of_path (p : Params) (hpath : Continuous (path p)) : SE2.ContinuousPath (frame p)

Continuity of the five-phase path implies componentwise continuity of the supporting SE(2) frame.

Continuity from the independent matching equations

structure GerverSofa.Romik.SwitchOrder (p : Params) : Prop

Ordering data needed to read the five branches in their intended order.

• phi_le_theta : p.phi ≤ p.theta
• theta_le_eta : p.theta ≤ Real.pi / 2 - p.theta
• eta_le_tau : Real.pi / 2 - p.theta ≤ Real.pi / 2 - p.phi

theorem GerverSofa.Romik.match_path12_of_equations {p : Params} (heq : Equations p) : path1 p p.phi = path2 p p.phi

Equation (35), extracted from the direct 22D system.

theorem GerverSofa.Romik.match_path23_of_equations {p : Params} (heq : Equations p) : path2 p p.theta = path3 p p.theta

Equation (37), extracted from the direct 22D system.

theorem GerverSofa.Romik.match_path34_of_equations {p : Params} (heq : Equations p) : path3 p (Real.pi / 2 - p.theta) = path4 p (Real.pi / 2 - p.theta)

Equation (39), extracted from the direct 22D system.

theorem GerverSofa.Romik.match_path45_of_equations {p : Params} (heq : Equations p) : path4 p (Real.pi / 2 - p.phi) = path5 p (Real.pi / 2 - p.phi)

Equation (41), extracted from the direct 22D system.

theorem GerverSofa.Romik.continuous_path_of_order_and_equations {p : Params} (hord : SwitchOrder p) (heq : Equations p) : Continuous (path p)

The four positional matching equations make the literal nested-if five-phase path continuous whenever its switches are ordered.

Exact real boxes used by the Krawczyk certificates

Every endpoint is written as an exact integer quotient. There are no binary floating-point constants in these definitions.

noncomputable def GerverSofa.qR (n : ℤ) (d : ℕ) : ℝ

Interpret an integer numerator and natural denominator as a real quotient.

Equations

• GerverSofa.qR n d = ↑n / ↑d

def GerverSofa.Reduced.box : Set Params

Input box X_a × X_b × X_phi × X_theta.

Equations

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

def GerverSofa.Romik.box : Set Params

The direct 22-dimensional box Y × Phi × Theta.

Equations

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

theorem GerverSofa.Romik.phi_pos_of_mem_box {p : Params} (hp : p ∈ box) : 0 < p.phi

Every point in the certified direct-system box has a positive first switching angle.

theorem GerverSofa.Romik.path_zero_of_mem_box_and_equations {p : Params} (hp : p ∈ box) (heq : Equations p) : path p 0 = (0, 0)

Equations (32)--(34), together with the certified box, force the exact initial path normalisation x(0)=(0,0).

theorem GerverSofa.Romik.switchOrder_of_mem_box {p : Params} (hp : p ∈ box) : SwitchOrder p

The exact direct-system box orders the four physical switching times.

theorem GerverSofa.Romik.continuous_path_of_mem_box_and_equations {p : Params} (hp : p ∈ box) (heq : Equations p) : Continuous (path p)

The certified box and the positional equations discharge the path continuity field needed by the moving-sofa assembly.

theorem GerverSofa.Romik.a1_lower_bound_of_mem_box {p : Params} (hp : p ∈ box) : 2420644844145377502832171437 / 2000000000000000000000000000 ≤ p.a1

The direct-system box supplies the strict lower bound on a₁ used in the area proposition.

Concrete Gerver cap, niche and fixed sofa

The definitions follow the manuscript literally. This file also proves the closedness part of the main topological certificate directly from the half-plane definitions; it does not use the numerical certificate or Baek's cap theory.

def GerverSofa.dot (p q : Point) : ℝ

Euclidean scalar product in the fixed coordinate representation.

Equations

• GerverSofa.dot p q = p.1 * q.1 + p.2 * q.2

noncomputable def GerverSofa.u (t : ℝ) : Point

Rotating outer-wall normals.

Equations

• GerverSofa.u t = (Real.cos t, Real.sin t)

noncomputable def GerverSofa.v (t : ℝ) : Point

The vertical unit vector rotated counterclockwise through angle t.

Equations

• GerverSofa.v t = (-Real.sin t, Real.cos t)

def GerverSofa.capFan : Set Point

The lower fan in the manuscript normalisation.

Equations

• GerverSofa.capFan = {q : GerverSofa.Point | 0 ≤ q.2}

def GerverSofa.supportHalfU (p : Romik.Params) (t : ℝ) : Set Point

First rotating supporting half-plane.

Equations

• GerverSofa.supportHalfU p t = {q : GerverSofa.Point | GerverSofa.dot q (GerverSofa.u t) ≤ GerverSofa.dot (GerverSofa.Romik.path p t) (GerverSofa.u t) + 1}

def GerverSofa.supportHalfV (p : Romik.Params) (t : ℝ) : Set Point

Second rotating supporting half-plane.

Equations

• GerverSofa.supportHalfV p t = {q : GerverSofa.Point | GerverSofa.dot q (GerverSofa.v t) ≤ GerverSofa.dot (GerverSofa.Romik.path p t) (GerverSofa.v t) + 1}

def GerverSofa.Romik.K0 (p : Params) : Set Point

The cap K₀ reconstructed from the five-phase path.

Equations

• GerverSofa.Romik.K0 p = {q : GerverSofa.Point | 0 ≤ q.2 ∧ ∀ t ∈ Set.Icc 0 (Real.pi / 2), q ∈ GerverSofa.supportHalfU p t ∩ GerverSofa.supportHalfV p t}

def GerverSofa.Romik.innerQuadrantAt (p : Params) (t : ℝ) : Set Point

Open inner quadrant of the supporting hallway at physical angle t.

Equations

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

def GerverSofa.Romik.innerUnion (p : Params) : Set Point

Union of all forbidden inner quadrants at interior rotation times.

Equations

• GerverSofa.Romik.innerUnion p = {q : GerverSofa.Point | ∃ t ∈ Set.Ioo 0 (Real.pi / 2), q ∈ GerverSofa.Romik.innerQuadrantAt p t}

def GerverSofa.Romik.niche (p : Params) : Set Point

The niche removed from the cap.

Equations

• GerverSofa.Romik.niche p = GerverSofa.capFan ∩ GerverSofa.Romik.innerUnion p

def GerverSofa.Romik.sofa (p : Params) : Set Point

The fixed Gerver candidate G = K₀ \ N(K₀).

Equations

• GerverSofa.Romik.sofa p = GerverSofa.Romik.K0 p \ GerverSofa.Romik.niche p

def GerverSofa.Romik.hallwayAt (p : Params) (s : ℝ) : Set Point

Physical supporting hallway at normalized time s.

Equations

• GerverSofa.Romik.hallwayAt p s = GerverSofa.supportingHallway (GerverSofa.Romik.frame p s)

Closedness facts independent of the numerical certificate

theorem GerverSofa.isClosed_supportHalfU (p : Romik.Params) (t : ℝ) : IsClosed (supportHalfU p t)

A fixed supporting half-plane is closed.

theorem GerverSofa.isClosed_supportHalfV (p : Romik.Params) (t : ℝ) : IsClosed (supportHalfV p t)

The other fixed supporting half-plane is closed.

theorem GerverSofa.isClosed_capFan : IsClosed capFan

The fan constraint is closed.

theorem GerverSofa.Romik.K0_eq_inter_iInter (p : Params) : K0 p = capFan ∩ ⋂ (t : { t : ℝ // t ∈ Set.Icc 0 (Real.pi / 2) }), supportHalfU p ↑t ∩ supportHalfV p ↑t

The bounded-quantifier definition of K₀ as an explicit intersection.

theorem GerverSofa.Romik.isClosed_K0 (p : Params) : IsClosed (K0 p)

K₀ is closed, before any support-maximisation or compactness argument.

theorem GerverSofa.Romik.isOpen_innerQuadrantAt (p : Params) (t : ℝ) : IsOpen (innerQuadrantAt p t)

Every instantaneous inner quadrant is open.

theorem GerverSofa.Romik.isOpen_innerUnion (p : Params) : IsOpen (innerUnion p)

The union of all interior-time inner quadrants is open.

theorem GerverSofa.Romik.K0_subset_capFan (p : Params) : K0 p ⊆ capFan

The cap lies in its fan by definition.

theorem GerverSofa.Romik.sofa_eq_K0_diff_innerUnion (p : Params) : sofa p = K0 p \ innerUnion p

Since K₀ ⊆ capFan, removing the niche is the same as removing the open union of forbidden quadrants.

theorem GerverSofa.Romik.isClosed_sofa (p : Params) : IsClosed (sofa p)

The concrete fixed sofa candidate is closed for every parameter vector.

Algebraic hallway characterisation and endpoint assembly

@[simp]

theorem GerverSofa.Romik.mem_supportHalfU (p : Params) (t : ℝ) (q : Point) : q ∈ supportHalfU p t ↔ dot q (u t) ≤ dot (path p t) (u t) + 1

@[simp]

theorem GerverSofa.Romik.mem_supportHalfV (p : Params) (t : ℝ) (q : Point) : q ∈ supportHalfV p t ↔ dot q (v t) ≤ dot (path p t) (v t) + 1

@[simp]

theorem GerverSofa.Romik.mem_K0 (p : Params) (q : Point) : q ∈ K0 p ↔ 0 ≤ q.2 ∧ ∀ t ∈ Set.Icc 0 (Real.pi / 2), q ∈ supportHalfU p t ∩ supportHalfV p t

@[simp]

theorem GerverSofa.Romik.mem_innerUnion (p : Params) (q : Point) : q ∈ innerUnion p ↔ ∃ t ∈ Set.Ioo 0 (Real.pi / 2), q ∈ innerQuadrantAt p t

@[simp]

theorem GerverSofa.Romik.mem_niche (p : Params) (q : Point) : q ∈ niche p ↔ q ∈ capFan ∧ q ∈ innerUnion p

@[simp]

theorem GerverSofa.Romik.mem_sofa (p : Params) (q : Point) : q ∈ sofa p ↔ q ∈ K0 p ∧ q ∉ niche p

theorem GerverSofa.Romik.frame_inv_act_formula (p : Params) (s : ℝ) (q : Point) : (frame p s).inv.act q = (dot (q.1 - (path p (angle s)).1, q.2 - (path p (angle s)).2) (u (angle s)), dot (q.1 - (path p (angle s)).1, q.2 - (path p (angle s)).2) (v (angle s)))

The inverse supporting frame has exactly the two signed wall coordinates used in the manuscript.

theorem GerverSofa.Romik.mem_hallwayAt_iff_wall_coordinates (p : Params) (s : ℝ) (q : Point) : q ∈ hallwayAt p s ↔ have t := angle s; have x := path p t; (dot (q.1 - x.1, q.2 - x.2) (u t) ≤ 1 ∧ dot (q.1 - x.1, q.2 - x.2) (v t) ≤ 1) ∧ ¬(dot (q.1 - x.1, q.2 - x.2) (u t) < 0 ∧ dot (q.1 - x.1, q.2 - x.2) (v t) < 0)

A point is in the supporting hallway iff its two wall coordinates lie in Q⁺ but not simultaneously in the open inner quadrant Q⁻.

theorem GerverSofa.Romik.not_mem_innerQuadrantAt_of_mem_sofa (p : Params) {q : Point} (hq : q ∈ sofa p) {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : q ∉ innerQuadrantAt p t

A sofa point cannot lie in an instantaneous forbidden quadrant at an interior physical time.

theorem GerverSofa.Romik.not_mem_initial_innerQuadrant (p : Params) (hzero : path p 0 = (0, 0)) {q : Point} (hq : q ∈ sofa p) : q ∉ innerQuadrantAt p 0

The lower-fan constraint excludes the initial inner quadrant once the physical path starts at the origin.

theorem GerverSofa.Romik.not_mem_final_innerQuadrant (p : Params) (hend : (path p (Real.pi / 2)).2 = 0) {q : Point} (hq : q ∈ sofa p) : q ∉ innerQuadrantAt p (Real.pi / 2)

The lower-fan constraint excludes the final inner quadrant once the final path point has second coordinate zero.

theorem GerverSofa.Romik.sofa_subset_hallwayAt (p : Params) (hzero : path p 0 = (0, 0)) (hend : (path p (Real.pi / 2)).2 = 0) (s : ℝ) : s ∈ Set.Icc 0 1 → sofa p ⊆ hallwayAt p s

The concrete cap-minus-niche set lies in every supporting hallway. The only endpoint input is the pair of path normalisations used in the paper.

theorem GerverSofa.Romik.initial_arm_of_path_zero (p : Params) (hzero : path p 0 = (0, 0)) : (frame p 0).inv.act '' sofa p ⊆ horizontalArm

The inverse frame at time zero places the concrete sofa in the horizontal arm.

theorem GerverSofa.Romik.final_arm_of_path_end_y_zero (p : Params) (hend : (path p (Real.pi / 2)).2 = 0) : (frame p 1).inv.act '' sofa p ⊆ verticalArm

The inverse frame at time one places the concrete sofa in the vertical arm.

Gerver sofa dependency batch

• KernelOnly.AlternatingSeries.
• KernelOnly.Coordinates.
• KernelOnly.EndpointSymmetry.
• KernelOnly.Identification.
• KernelOnly.ReplayConsequences.
• KernelOnly.SoundnessInterfaces.
• KernelOnly.TranscendentalSoundness.
• KernelOnly.ADCoreSoundness.
• KernelOnly.ReducedADSoundness.
• KernelOnly.FullADSoundness.

Alternating-series kernel for the executable transcendental layer

This file connects the exact rational partial sums used by ExactReplay to Mathlib's real power-series theorems. The Taylor evaluator is intentionally used only on arguments in [0, 1]; the range-reduction layer proves this precondition before calling these results.

noncomputable def GerverSofa.ExactReplay.sinMagnitude (x : ℝ) (n : ℕ) : ℝ

Real magnitude of the nth sine-series term.

Equations

• GerverSofa.ExactReplay.sinMagnitude x n = x ^ (2 * n + 1) / ↑(2 * n + 1).factorial

noncomputable def GerverSofa.ExactReplay.cosMagnitude (x : ℝ) (n : ℕ) : ℝ

Real magnitude of the nth cosine-series term.

Equations

• GerverSofa.ExactReplay.cosMagnitude x n = x ^ (2 * n) / ↑(2 * n).factorial

noncomputable def GerverSofa.ExactReplay.atanMagnitude (x : ℝ) (n : ℕ) : ℝ

Real magnitude of the nth arctangent-series term.

Equations

• GerverSofa.ExactReplay.atanMagnitude x n = x ^ (2 * n + 1) / ↑(2 * n + 1)

theorem GerverSofa.ExactReplay.antitone_sinMagnitude {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : Antitone (sinMagnitude x)

On [0,1], the unsigned sine Taylor terms decrease.

theorem GerverSofa.ExactReplay.antitone_cosMagnitude {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : Antitone (cosMagnitude x)

On [0,1], the unsigned cosine Taylor terms decrease.

theorem GerverSofa.ExactReplay.antitone_atanMagnitude {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : Antitone (atanMagnitude x)

On [0,1], the unsigned arctangent Taylor terms decrease.

theorem GerverSofa.ExactReplay.coe_sinPartial (x : ℚ) (terms : ℕ) : ↑(sinPartial x terms) = ∑ k ∈ Finset.range terms, (-1) ^ k * ↑x ^ (2 * k + 1) / ↑(2 * k + 1).factorial

Casting the executable sine partial sum to ℝ gives the corresponding Mathlib finite Taylor sum.

theorem GerverSofa.ExactReplay.coe_cosPartial (x : ℚ) (terms : ℕ) : ↑(cosPartial x terms) = ∑ k ∈ Finset.range terms, (-1) ^ k * ↑x ^ (2 * k) / ↑(2 * k).factorial

Casting the executable cosine partial sum to ℝ gives the corresponding Mathlib finite Taylor sum.

theorem GerverSofa.ExactReplay.coe_atanPartial (x : ℚ) (terms : ℕ) : ↑(atanPartial x terms) = ∑ k ∈ Finset.range terms, (-1) ^ k * ↑x ^ (2 * k + 1) / ↑(2 * k + 1)

Casting the executable arctangent partial sum to ℝ gives the corresponding Mathlib finite Taylor sum.

theorem GerverSofa.ExactReplay.sine_between_partials {x : ℚ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : ↑(sinPartial x 20) ≤ Real.sin ↑x ∧ Real.sin ↑x ≤ ↑(sinPartial x 19)

The 20-term sine partial sum is a lower bound and the 19-term partial sum is an upper bound for every rational argument in [0,1].

theorem GerverSofa.ExactReplay.cosine_between_partials {x : ℚ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : ↑(cosPartial x 20) ≤ Real.cos ↑x ∧ Real.cos ↑x ≤ ↑(cosPartial x 19)

The 20-term cosine partial sum is a lower bound and the 19-term partial sum is an upper bound for every rational argument in [0,1].

theorem GerverSofa.ExactReplay.arctan_between_partials {x : ℚ} (hx0 : 0 ≤ x) (hx1 : x < 1) (k : ℕ) : ↑(atanPartial x (2 * k + 2)) ≤ Real.arctan ↑x ∧ Real.arctan ↑x ≤ ↑(atanPartial x (2 * k + 1))

Even/odd arctangent partial sums provide certified lower/upper bounds.

Coordinate equivalences for the certified systems

The executable interval layer works with Fin n → ℝ, while the manuscript layer uses named parameter records. These equivalences are the explicit, kernel-checked bridge between the two representations.

def GerverSofa.Reduced.coordEquiv : Params ≃ Vec 4

Named reduced parameters as a four-vector in manuscript order.

Equations

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

noncomputable def GerverSofa.Reduced.vectorSystem (x : Vec 4) : Vec 4

Reduced system expressed in finite-vector coordinates.

Equations

• GerverSofa.Reduced.vectorSystem x = GerverSofa.Reduced.system (GerverSofa.Reduced.coordEquiv.symm x)

def GerverSofa.Reduced.vectorBox : Set (Vec 4)

The reduced parameter box expressed in finite-vector coordinates.

Equations

• GerverSofa.Reduced.vectorBox = {x : GerverSofa.Vec 4 | GerverSofa.Reduced.coordEquiv.symm x ∈ GerverSofa.Reduced.box}

@[simp]

theorem GerverSofa.Reduced.mem_vectorBox_iff (x : Vec 4) : x ∈ vectorBox ↔ coordEquiv.symm x ∈ box

def GerverSofa.Reduced.uniqueSolutionOfVector (c : CertifiedUniqueZero vectorSystem vectorBox) : CertifiedUniqueSolution Equations box

Transport a finite-vector uniqueness certificate back to named reduced parameters.

Equations

• GerverSofa.Reduced.uniqueSolutionOfVector c = { solution := GerverSofa.Reduced.coordEquiv.symm c.solution, solution_mem := ⋯, satisfies := ⋯, unique_iff := ⋯ }

def GerverSofa.Romik.coordEquiv : Params ≃ Vec 22

Named Romik parameters as a 22-vector in verifier order.

Equations

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

noncomputable def GerverSofa.Romik.vectorSystem (x : Vec 22) : Vec 22

Direct Romik system expressed in finite-vector coordinates.

Equations

• GerverSofa.Romik.vectorSystem x = GerverSofa.Romik.system (GerverSofa.Romik.coordEquiv.symm x)

def GerverSofa.Romik.vectorBox : Set (Vec 22)

The direct Romik box expressed in finite-vector coordinates.

Equations

• GerverSofa.Romik.vectorBox = {x : GerverSofa.Vec 22 | GerverSofa.Romik.coordEquiv.symm x ∈ GerverSofa.Romik.box}

@[simp]

theorem GerverSofa.Romik.mem_vectorBox_iff (x : Vec 22) : x ∈ vectorBox ↔ coordEquiv.symm x ∈ box

def GerverSofa.Romik.uniqueSolutionOfVector (c : CertifiedUniqueZero vectorSystem vectorBox) : CertifiedUniqueSolution Equations box

Transport a finite-vector uniqueness certificate back to named Romik parameters.

Equations

• GerverSofa.Romik.uniqueSolutionOfVector c = { solution := GerverSofa.Romik.coordEquiv.symm c.solution, solution_mem := ⋯, satisfies := ⋯, unique_iff := ⋯ }

Endpoint symmetry derived from the direct 22-dimensional system

The manuscript obtains the terminal condition x₂(π/2)=0 from the reflection symmetry of the five phases. This file proves the required consequence without introducing a symmetry assumption and without using numerical approximations.

FIX12 keeps the BATCH11 mathematics and public theorem statements unchanged, but factors the formula-level algebra into small coordinate identities. This avoids asking ring to normalize the fully unfolded five-phase expressions in one large proof term.

Exact parameter consequences of equations 27--34

theorem GerverSofa.Romik.e1_eq_a1_of_equations {p : Params} (heq : Equations p) : p.e1 = p.a1

Equation 27.

theorem GerverSofa.Romik.e2_eq_neg_a2_of_equations {p : Params} (heq : Equations p) : p.e2 = -p.a2

Equation 28.

theorem GerverSofa.Romik.d1_eq_quarterPi_sub_b1_of_equations {p : Params} (heq : Equations p) : p.d1 = Real.pi / 4 - p.b1

Equation 29.

theorem GerverSofa.Romik.d2_eq_b2_add_quarterPi_correction_of_equations {p : Params} (heq : Equations p) : p.d2 = p.b2 + Real.pi / 4 * (2 * p.b1 - Real.pi / 4)

Equation 30.

theorem GerverSofa.Romik.c2_eq_c1_sub_halfPi_of_equations {p : Params} (heq : Equations p) : p.c2 = p.c1 - Real.pi / 2

Equation 31.

theorem GerverSofa.Romik.k12_eq_quarter_of_equations {p : Params} (heq : Equations p) : p.k12 = 1 / 4

Equation 33.

theorem GerverSofa.Romik.a2_eq_neg_quarter_of_equations {p : Params} (heq : Equations p) : p.a2 = -(1 / 4)

Equation 34.

theorem GerverSofa.Romik.e2_eq_quarter_of_equations {p : Params} (heq : Equations p) : p.e2 = 1 / 4

Equations 28 and 34.

Small definitional coordinate identities

These are deliberately rfl: they expose only the second coordinate of one phase at a time. Downstream algebra therefore operates on compact scalar expressions rather than on the fully unfolded Point/rot/addK terms.

Formula-level reflection identities

theorem GerverSofa.Romik.phase15_vertical_reflection_of_equations {p : Params} (heq : Equations p) (t : ℝ) : (path5 p (Real.pi / 2 - t)).2 - p.k52 = (path1 p t).2 - p.k12

The vertical phase-5 formula at reflected time differs from phase 1 only by its vertical translation constant.

theorem GerverSofa.Romik.phase24_vertical_reflection_of_equations {p : Params} (heq : Equations p) (t : ℝ) : (path4 p (Real.pi / 2 - t)).2 - p.k42 = (path2 p t).2 - p.k22

The vertical phase-4 formula at reflected time differs from phase 2 only by its vertical translation constant.

theorem GerverSofa.Romik.phase3_vertical_reflection_of_equations {p : Params} (heq : Equations p) (t : ℝ) : (path3 p (Real.pi / 2 - t)).2 = (path3 p t).2

The middle phase has exact vertical reflection symmetry.

Translation constants forced by matching

theorem GerverSofa.Romik.k42_eq_k22_of_equations {p : Params} (heq : Equations p) : p.k42 = p.k22

Matching at θ and π/2-θ, together with middle-phase reflection, forces the phase-2 and phase-4 vertical translations to coincide.

theorem GerverSofa.Romik.k52_eq_k12_of_equations {p : Params} (heq : Equations p) : p.k52 = p.k12

Matching at φ and π/2-φ then forces the phase-1 and phase-5 vertical translations to coincide.

theorem GerverSofa.Romik.k52_eq_quarter_of_equations {p : Params} (heq : Equations p) : p.k52 = 1 / 4

Equations 27--41 force the previously dependent coefficient k₅₂=1/4. It is not an independent hypothesis of the final certificate.

Terminal condition

theorem GerverSofa.Romik.path5_end_y_zero_of_equations {p : Params} (heq : Equations p) : (path5 p (Real.pi / 2)).2 = 0

The explicit fifth phase ends at vertical coordinate zero.

theorem GerverSofa.Romik.path_halfPi_eq_path5_of_mem_box {p : Params} (hp : p ∈ box) : path p (Real.pi / 2) = path5 p (Real.pi / 2)

The certified direct-system box places π/2 strictly after the fourth switch, so the literal nested-if path uses phase 5 at the endpoint.

theorem GerverSofa.Romik.path_end_y_zero_of_mem_box_and_equations {p : Params} (hp : p ∈ box) (heq : Equations p) : (path p (Real.pi / 2)).2 = 0

The terminal vertical normalisation is a theorem of the concrete box and 22 equations. No reflection hypothesis and no certificate field remain.

Identification with Romik's hallway-intersection reconstruction

This is the set-theoretic part of Proposition prop:gerver. It uses only the literal definitions and the two endpoint normalisations; the eighteen-piece boundary statement remains a separate field of FullArticleCertificate.

def GerverSofa.Romik.reconstructedSet (p : Params) : Set Point

Romik's fixed-frame reconstruction: initial arm, every supporting hallway, and the final transported vertical arm.

Equations

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

noncomputable def GerverSofa.Romik.normalizedTime (t : ℝ) : ℝ

Convert a physical angle in [0,π/2] to normalized time.

Equations

• GerverSofa.Romik.normalizedTime t = t / (Real.pi / 2)

@[simp]

theorem GerverSofa.Romik.angle_normalizedTime (t : ℝ) : angle (normalizedTime t) = t

theorem GerverSofa.Romik.normalizedTime_mem_unit {t : ℝ} (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : normalizedTime t ∈ Set.Icc 0 1

theorem GerverSofa.Romik.sofa_subset_reconstructedSet (p : Params) (hzero : path p 0 = (0, 0)) (hend : (path p (Real.pi / 2)).2 = 0) : sofa p ⊆ reconstructedSet p

Every point of the cap-minus-niche set lies in Romik's hallway intersection reconstruction.

theorem GerverSofa.Romik.mem_K0_of_mem_all_hallways (p : Params) {q : Point} (hbase : 0 ≤ q.2) (hall : ∀ s ∈ Set.Icc 0 1, q ∈ hallwayAt p s) : q ∈ K0 p

Membership in every physical supporting hallway gives all outer support inequalities in the cap definition.

theorem GerverSofa.Romik.not_mem_innerUnion_of_mem_all_hallways (p : Params) {q : Point} (hall : ∀ s ∈ Set.Icc 0 1, q ∈ hallwayAt p s) : q ∉ innerUnion p

Membership in every physical hallway excludes every open interior-time inner quadrant.

theorem GerverSofa.Romik.reconstructedSet_subset_sofa (p : Params) : reconstructedSet p ⊆ sofa p

Conversely, Romik's hallway intersection lies in the concrete cap-minus-niche set.

theorem GerverSofa.Romik.sofa_eq_reconstructedSet (p : Params) (hzero : path p 0 = (0, 0)) (hend : (path p (Real.pi / 2)).2 = 0) : sofa p = reconstructedSet p

Set-theoretic identification G = Sₓ, conditional only on the endpoint normalisations already isolated by the main certificate.

Named consequences of the frozen kernel-only certificate

These handles intentionally reason about the proof-carrying rational data, not about re-running the expensive Krawczyk/grid search inside kernel reduction. The latter remains available under ExactReplay.executable* for independent diagnostic comparison.

theorem GerverSofa.CertificateManifest.machin_inside_declared : machinPi.strictInsideB declaredPi = true

Semantic interfaces for the executable interval certificate

These definitions state, without hiding any mathematical assumption, the bridges that turn the frozen rational replay into facts about Real.sin, Real.cos, the two real systems, and their Jacobians. Concrete proof terms for these interfaces are the remaining analytic part of the end-to-end certificate; no axiom is declared here.

def GerverSofa.EnclosesVec {n : ℕ} (box : List RatInterval) (x : Vec n) : Prop

A rational interval list encloses a finite real vector coordinatewise.

Equations

• GerverSofa.EnclosesVec box x = (box.length = n ∧ ∀ (i : Fin n), (box.getD (↑i) (GerverSofa.RatInterval.point 0)).Contains (x i))

def GerverSofa.RealDerivativeAt (f : ℝ → ℝ) (f' x : ℝ) : Prop

A one-dimensional real derivative certificate in the classical difference-quotient form. This is the exact real specialization of the right-hand side of Mathlib's hasDerivAt_iff_tendsto_slope_zero: it states that (f (x+t)-f x)/t tends to f' as t → 0, t ≠ 0.

Unlike storing raw HasDerivAt/DifferentiableAt, this proposition contains no hidden AddCommGroup/Module instance path for the codomain ℝ; this removes the instance diamond exposed by Lean 4.33 while retaining the full mathematical meaning of an actual derivative.

Equations

• GerverSofa.RealDerivativeAt f f' x = Filter.Tendsto (fun (t : ℝ) => t⁻¹ * (f (x + t) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds f')

structure GerverSofa.TranscendentalSoundness : Prop

Exact analytic correctness required from the executable trigonometric layer. The domain is the physical range used by the Gerver certificate.

• pi_mem : ExactReplay.declaredPiInterval.Contains Real.pi
• sine_mem (z : RatInterval) (x : ℝ) : z.Contains x → 0 ≤ x → x ≤ Real.pi / 2 → (ExactReplay.sineInterval z).Contains (Real.sin x)
• cosine_mem (z : RatInterval) (x : ℝ) : z.Contains x → 0 ≤ x → x ≤ Real.pi / 2 → (ExactReplay.cosineInterval z).Contains (Real.cos x)

Soundness of the exact transcendental interval evaluator

This file proves the analytic trust bridge omitted by the executable replay:

• the alternating rational arctangent sums enclose the two Machin terms;
• the computed Machin interval encloses Real.pi and lies in the declared interval;
• fixed-decimal rounding is outward;
• the small-argument Taylor intervals enclose Real.sin and Real.cos;
• complementary-angle reduction is sound on [0, π/2];
• externally over-wide intervals fail closed to [-1,1] rather than silently violating the Taylor precondition.

No project axiom and no floating-point literal occurs in this file.

Partial-sum interval consequences

theorem GerverSofa.ExactReplay.sinBound_contains {x : ℚ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : (sinBound x).Contains (Real.sin ↑x)

The executable sine Taylor hull contains the exact real sine value on [0,1].

theorem GerverSofa.ExactReplay.cosBound_contains {x : ℚ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : (cosBound x).Contains (Real.cos ↑x)

The executable cosine Taylor hull contains the exact real cosine value on [0,1].

theorem GerverSofa.ExactReplay.atanBound_contains {x : ℚ} (hx0 : 0 ≤ x) (hx1 : x < 1) (k : ℕ) : (atanBound x (2 * k + 1) (2 * k + 2)).Contains (Real.arctan ↑x)

Consecutive odd/even arctangent sums form a semantic interval.

Machin identity and the declared interval for π

theorem GerverSofa.ExactReplay.machinPi_contains_pi : machinPi.Contains Real.pi

The interval computed from the two exact arctangent Taylor certificates contains the true value of π.

theorem GerverSofa.ExactReplay.machinPi_eq_manifest : machinPi = CertificateManifest.machinPi

theorem GerverSofa.ExactReplay.piI_eq_manifest : piI = CertificateManifest.declaredPi

The executable declared interval agrees with the frozen manifest.

theorem GerverSofa.ExactReplay.piI_contains_pi : piI.Contains Real.pi

The exact interval used by every transcendental call encloses Real.pi.

Outward decimal rounding

theorem GerverSofa.ExactReplay.floorDecimal_le (x : ℚ) (digits : ℕ := 60) : floorDecimal x digits ≤ x

Fixed-decimal floor rounding never exceeds the input rational.

theorem GerverSofa.ExactReplay.le_ceilDecimal (x : ℚ) (digits : ℕ := 60) : x ≤ ceilDecimal x digits

Fixed-decimal ceiling rounding never lies below the input rational.

theorem GerverSofa.ExactReplay.outwardDecimal_contains {z : RatInterval} {x : ℝ} (hx : z.Contains x) : (outwardDecimal z).Contains x

The exact 60-decimal conversion is outward in real semantics.

Small-argument sine and cosine

theorem GerverSofa.ExactReplay.sinSmall_contains {z : RatInterval} {x : ℝ} (hx : z.Contains x) (hz0 : 0 ≤ z.lo) (hz9 : z.hi ≤ 9 / 10) : (sinSmall z).Contains (Real.sin x)

The small sine evaluator is sound whenever its whole input lies in [0, 9/10].

theorem GerverSofa.ExactReplay.cosSmall_contains {z : RatInterval} {x : ℝ} (hx : z.Contains x) (hz0 : 0 ≤ z.lo) (hz9 : z.hi ≤ 9 / 10) : (cosSmall z).Contains (Real.cos x)

The small cosine evaluator is sound whenever its whole input lies in [0, 9/10].

Range reduction and fail-closed totality

theorem GerverSofa.ExactReplay.physicalClamp_contains {z : RatInterval} {x : ℝ} (hz : z.Contains x) (hx0 : 0 ≤ x) (hxpi : x ≤ Real.pi / 2) : (physicalClamp z).Contains x

Physical clamping preserves every enclosed angle in [0,π/2].

theorem GerverSofa.ExactReplay.complementInterval_contains {z : RatInterval} {x : ℝ} (hz : z.Contains x) (hxpi : x ≤ Real.pi / 2) : (complementInterval z).Contains (Real.pi / 2 - x)

Complementary-angle range reduction encloses π/2-x.

theorem GerverSofa.ExactReplay.universal_contains_sin (x : ℝ) : universalTrigInterval.Contains (Real.sin x)

Universal fallback for sine.

theorem GerverSofa.ExactReplay.universal_contains_cos (x : ℝ) : universalTrigInterval.Contains (Real.cos x)

Universal fallback for cosine.

theorem GerverSofa.ExactReplay.sinI_contains {z : RatInterval} {x : ℝ} (hz : z.Contains x) (hx0 : 0 ≤ x) (hxpi : x ≤ Real.pi / 2) : (sinI z).Contains (Real.sin x)

Full soundness of the executable sine interval on the physical angular range.

theorem GerverSofa.ExactReplay.cosI_contains {z : RatInterval} {x : ℝ} (hz : z.Contains x) (hx0 : 0 ≤ x) (hxpi : x ≤ Real.pi / 2) : (cosI z).Contains (Real.cos x)

Full soundness of the executable cosine interval on the physical angular range.

Structural soundness of first-order interval automatic differentiation

The executable ExactReplay.D object stores a value interval and one interval for every first partial derivative. This file supplies the reusable semantic induction for all constructors actually used by the 4D and 22D certificates. The concrete systems are handled in a separate module by instantiating these constructor theorems.

Smooth scalar models

structure GerverSofa.ScalarModel (n : ℕ) : Type

A scalar function together with its coordinate gradient and a proof that those coordinates are the actual partial derivatives. The derivative witness is stored as RealDerivativeAt, a first-principles real difference-quotient limit. Constructor proofs temporarily move through Mathlib's HasDerivAt API and immediately return to this instance-stable semantic proposition.

• value : Vec n → ℝ

  The real scalar function represented by the model.

• gradient : Vec n → Vec n

  The coordinate gradient of the scalar function.

• hasDeriv_update (x : Fin n → ℝ) (j : Fin n) : RealDerivativeAt (fun (t : ℝ) => self.value (Function.update x j t)) (self.gradient x j) (x j)

def GerverSofa.ScalarModel.const (n : ℕ) (c : ℝ) : ScalarModel n

Constant scalar model.

Equations

• GerverSofa.ScalarModel.const n c = { value := fun (x : GerverSofa.Vec n) => c, gradient := fun (x : GerverSofa.Vec n) (x_1 : Fin n) => 0, hasDeriv_update := ⋯ }

def GerverSofa.ScalarModel.var (n : ℕ) (k : Fin n) : ScalarModel n

Coordinate projection.

Equations

• GerverSofa.ScalarModel.var n k = { value := fun (x : GerverSofa.Vec n) => x k, gradient := fun (x : GerverSofa.Vec n) (j : Fin n) => if j = k then 1 else 0, hasDeriv_update := ⋯ }

def GerverSofa.ScalarModel.add {n : ℕ} (f g : ScalarModel n) : ScalarModel n

Pointwise addition.

Equations

• f.add g = { value := fun (x : GerverSofa.Vec n) => f.value x + g.value x, gradient := fun (x : GerverSofa.Vec n) (j : Fin n) => f.gradient x j + g.gradient x j, hasDeriv_update := ⋯ }

def GerverSofa.ScalarModel.neg {n : ℕ} (f : ScalarModel n) : ScalarModel n

Pointwise negation.

Equations

• f.neg = { value := fun (x : GerverSofa.Vec n) => -f.value x, gradient := fun (x : GerverSofa.Vec n) (j : Fin n) => -f.gradient x j, hasDeriv_update := ⋯ }

def GerverSofa.ScalarModel.sub {n : ℕ} (f g : ScalarModel n) : ScalarModel n

Pointwise subtraction.

Equations

• f.sub g = f.add g.neg

def GerverSofa.ScalarModel.mul {n : ℕ} (f g : ScalarModel n) : ScalarModel n

Pointwise multiplication.

Equations

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

def GerverSofa.ScalarModel.scale {n : ℕ} (a : ℚ) (f : ScalarModel n) : ScalarModel n

Rational scaling.

Equations

• GerverSofa.ScalarModel.scale a f = { value := fun (x : GerverSofa.Vec n) => ↑a * f.value x, gradient := fun (x : GerverSofa.Vec n) (j : Fin n) => ↑a * f.gradient x j, hasDeriv_update := ⋯ }

noncomputable def GerverSofa.ScalarModel.sin {n : ℕ} (f : ScalarModel n) : ScalarModel n

Sine composition.

Equations

• f.sin = { value := fun (x : GerverSofa.Vec n) => Real.sin (f.value x), gradient := fun (x : GerverSofa.Vec n) (j : Fin n) => Real.cos (f.value x) * f.gradient x j, hasDeriv_update := ⋯ }

noncomputable def GerverSofa.ScalarModel.cos {n : ℕ} (f : ScalarModel n) : ScalarModel n

Cosine composition.

Equations

• f.cos = { value := fun (x : GerverSofa.Vec n) => Real.cos (f.value x), gradient := fun (x : GerverSofa.Vec n) (j : Fin n) => -Real.sin (f.value x) * f.gradient x j, hasDeriv_update := ⋯ }

@[instance_reducible]

instance GerverSofa.ScalarModel.instAdd {n : ℕ} : Add (ScalarModel n)

Equations

• GerverSofa.ScalarModel.instAdd = { add := GerverSofa.ScalarModel.add }

@[instance_reducible]

instance GerverSofa.ScalarModel.instNeg {n : ℕ} : Neg (ScalarModel n)

Equations

• GerverSofa.ScalarModel.instNeg = { neg := GerverSofa.ScalarModel.neg }

@[instance_reducible]

instance GerverSofa.ScalarModel.instSub {n : ℕ} : Sub (ScalarModel n)

Equations

• GerverSofa.ScalarModel.instSub = { sub := GerverSofa.ScalarModel.sub }

@[instance_reducible]

instance GerverSofa.ScalarModel.instMul {n : ℕ} : Mul (ScalarModel n)

Equations

• GerverSofa.ScalarModel.instMul = { mul := GerverSofa.ScalarModel.mul }

@[instance_reducible]

instance GerverSofa.ScalarModel.instHMulRat {n : ℕ} : HMul ℚ (ScalarModel n) (ScalarModel n)

Equations

• GerverSofa.ScalarModel.instHMulRat = { hMul := GerverSofa.ScalarModel.scale }

The executable systems are written with notation, while constructor-level soundness lemmas produce the named operations above. These tiny simp bridges make that definitional equality explicit without unfolding the proof-carrying structures themselves.

@[simp]

theorem GerverSofa.ScalarModel.add_notation {n : ℕ} (f g : ScalarModel n) : f + g = f.add g

@[simp]

theorem GerverSofa.ScalarModel.neg_notation {n : ℕ} (f : ScalarModel n) : -f = f.neg

@[simp]

theorem GerverSofa.ScalarModel.sub_notation {n : ℕ} (f g : ScalarModel n) : f - g = f.sub g

@[simp]

theorem GerverSofa.ScalarModel.mul_notation {n : ℕ} (f g : ScalarModel n) : f * g = f.mul g

@[simp]

theorem GerverSofa.ScalarModel.scale_notation {n : ℕ} (a : ℚ) (f : ScalarModel n) : a * f = scale a f

@[simp]

theorem GerverSofa.ScalarModel.add_value {n : ℕ} (f g : ScalarModel n) (x : Vec n) : (f.add g).value x = f.value x + g.value x

@[simp]

theorem GerverSofa.ScalarModel.neg_value {n : ℕ} (f : ScalarModel n) (x : Vec n) : f.neg.value x = -f.value x

@[simp]

theorem GerverSofa.ScalarModel.sub_value {n : ℕ} (f g : ScalarModel n) (x : Vec n) : (f.sub g).value x = f.value x - g.value x

@[simp]

theorem GerverSofa.ScalarModel.mul_value {n : ℕ} (f g : ScalarModel n) (x : Vec n) : (f.mul g).value x = f.value x * g.value x

@[simp]

theorem GerverSofa.ScalarModel.scale_value {n : ℕ} (a : ℚ) (f : ScalarModel n) (x : Vec n) : (scale a f).value x = ↑a * f.value x

@[simp]

theorem GerverSofa.ScalarModel.sin_value {n : ℕ} (f : ScalarModel n) (x : Vec n) : f.sin.value x = Real.sin (f.value x)

@[simp]

theorem GerverSofa.ScalarModel.cos_value {n : ℕ} (f : ScalarModel n) (x : Vec n) : f.cos.value x = Real.cos (f.value x)

Matching notation bridges for the executable dual intervals.

@[simp]

theorem GerverSofa.ExactReplay.D.add_notation (x y : D) : x + y = x.addD y

@[simp]

theorem GerverSofa.ExactReplay.D.neg_notation (x : D) : -x = x.negD

@[simp]

theorem GerverSofa.ExactReplay.D.sub_notation (x y : D) : x - y = x.subD y

@[simp]

theorem GerverSofa.ExactReplay.D.mul_notation (x y : D) : x * y = x.mulD y

@[simp]

theorem GerverSofa.ExactReplay.D.scale_notation (a : ℚ) (x : D) : a * x = scaleD a x

Semantic relation for the executable dual interval

structure GerverSofa.DSoundOn {n : ℕ} (X : Set (Vec n)) (d : ExactReplay.D) (f : ScalarModel n) : Prop

An executable dual interval encloses a smooth scalar model on a set.

• value_sound (x : Vec n) : x ∈ X → d.val.Contains (f.value x)
• derivative_length : d.der.length = n
• derivative_sound (x : Vec n) : x ∈ X → ∀ (j : Fin n), (d.der.getD (↑j) ExactReplay.zeroI).Contains (f.gradient x j)

List access lemmas used by the AD constructors

Constructor soundness

theorem GerverSofa.DSoundOn.const {n : ℕ} {X : Set (Vec n)} {z : RatInterval} {c : ℝ} (hc : z.Contains c) : DSoundOn X (ExactReplay.D.const z n) (ScalarModel.const n c)

Exact interval constant.

theorem GerverSofa.DSoundOn.pointConst {n : ℕ} {X : Set (Vec n)} (q : ℚ) : DSoundOn X (ExactReplay.D.pointConst q n) (ScalarModel.const n ↑q)

Rational point constant.

theorem GerverSofa.DSoundOn.varD {n : ℕ} {X : Set (Vec n)} (input : RatInterval) (k : Fin n) (hinput : ∀ x ∈ X, input.Contains (x k)) : DSoundOn X (ExactReplay.D.varD input (↑k) n) (ScalarModel.var n k)

Coordinate variable read from an enclosing input interval.

theorem GerverSofa.DSoundOn.add {n : ℕ} {X : Set (Vec n)} {dx dy : ExactReplay.D} {f g : ScalarModel n} (hx : DSoundOn X dx f) (hy : DSoundOn X dy g) : DSoundOn X (dx.addD dy) (f.add g)

Addition constructor.

theorem GerverSofa.DSoundOn.neg {n : ℕ} {X : Set (Vec n)} {d : ExactReplay.D} {f : ScalarModel n} (h : DSoundOn X d f) : DSoundOn X d.negD f.neg

Negation constructor.

theorem GerverSofa.DSoundOn.sub {n : ℕ} {X : Set (Vec n)} {dx dy : ExactReplay.D} {f g : ScalarModel n} (hx : DSoundOn X dx f) (hy : DSoundOn X dy g) : DSoundOn X (dx.subD dy) (f.sub g)

Subtraction constructor.

theorem GerverSofa.DSoundOn.mul {n : ℕ} {X : Set (Vec n)} {dx dy : ExactReplay.D} {f g : ScalarModel n} (hx : DSoundOn X dx f) (hy : DSoundOn X dy g) : DSoundOn X (dx.mulD dy) (f.mul g)

Multiplication constructor and product rule.

theorem GerverSofa.DSoundOn.scale {n : ℕ} {X : Set (Vec n)} (a : ℚ) {d : ExactReplay.D} {f : ScalarModel n} (h : DSoundOn X d f) : DSoundOn X (ExactReplay.D.scaleD a d) (ScalarModel.scale a f)

Rational scaling constructor.

theorem GerverSofa.DSoundOn.sin {n : ℕ} {X : Set (Vec n)} {d : ExactReplay.D} {f : ScalarModel n} (h : DSoundOn X d f) (hphysical : ∀ x ∈ X, 0 ≤ f.value x ∧ f.value x ≤ Real.pi / 2) : DSoundOn X d.sinD f.sin

Sine constructor and chain rule.

theorem GerverSofa.DSoundOn.cos {n : ℕ} {X : Set (Vec n)} {d : ExactReplay.D} {f : ScalarModel n} (h : DSoundOn X d f) (hphysical : ∀ x ∈ X, 0 ≤ f.value x ∧ f.value x ≤ Real.pi / 2) : DSoundOn X d.cosD f.cos

Cosine constructor and chain rule.

Concrete interval-AD soundness for the reduced 4D system

This module instantiates the constructor-level AD theorem with equations (F1)--(F4), proves that the frozen rational list is exactly the manuscript box, and identifies the four smooth scalar models with Reduced.vectorSystem.

theorem GerverSofa.Reduced.inputBox_exact (x : Vec 4) : x ∈ vectorBox ↔ EnclosesVec ExactReplay.reducedInputBox x

The four frozen rational intervals are exactly the named reduced box.

noncomputable def GerverSofa.Reduced.models : Fin 4 → ScalarModel 4

Scalar models matching the four reduced equations.

Equations

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

theorem GerverSofa.Reduced.vectorSystem_eq_models (x : Vec 4) : vectorSystem x = fun (i : Fin 4) => (models i).value x

The model values are definitionally the manuscript reduced system after coordinate conversion.

Concrete interval-AD soundness for the direct 22D Romik system

The direct system contains five trigonometric path pieces, three derivative pieces and six matching pairs. To avoid 22 unrelated derivative proofs, this file evaluates every expression in a proof-carrying dual object. Its first projection is the exact executable ExactReplay.D; its second projection is a smooth real scalar model; and its third field is the constructor-level soundness theorem from ADCoreSoundness.

Exact identification of the 22D input box

The 22 coordinates are kept as separate tiny lemmas. This is deliberately chunked: expanding all 44 rational endpoint inequalities in one simp call exhausts the default heartbeat budget even though every coordinate identity is individually trivial.

theorem GerverSofa.Romik.inputBox_exact (x : Vec 22) : x ∈ vectorBox ↔ EnclosesVec ExactReplay.fullInputBox x

The 22 frozen rational intervals are exactly the named direct-system box.

theorem GerverSofa.Romik.full_switches_physical {x : Vec 22} (hx : x ∈ vectorBox) : (0 ≤ x 20 ∧ x 20 ≤ Real.pi / 2) ∧ (0 ≤ x 21 ∧ x 21 ≤ Real.pi / 2) ∧ (0 ≤ Real.pi / 2 - x 21 ∧ Real.pi / 2 - x 21 ≤ Real.pi / 2) ∧ 0 ≤ Real.pi / 2 - x 20 ∧ Real.pi / 2 - x 20 ≤ Real.pi / 2

All four switching times used by the direct evaluator lie in [0,π/2].

Proof-carrying dual expressions

structure GerverSofa.Romik.SoundDual (n : ℕ) (X : Set (Vec n)) : Type

One executable interval dual paired with its real semantic model.

• d : ExactReplay.D

  The interval value and derivative data being certified.

• model : ScalarModel n

  The real scalar function and gradient represented by the interval data.

• sound : DSoundOn X self.d self.model

def GerverSofa.Romik.SoundDual.const {n : ℕ} {X : Set (Vec n)} (z : RatInterval) (c : ℝ) (h : z.Contains c) : SoundDual n X

A constant scalar model with a certified interval enclosure.

Equations

• GerverSofa.Romik.SoundDual.const z c h = { d := GerverSofa.ExactReplay.D.const z n, model := GerverSofa.ScalarModel.const n c, sound := ⋯ }

def GerverSofa.Romik.SoundDual.pointConst {n : ℕ} {X : Set (Vec n)} (q : ℚ) : SoundDual n X

A rational constant represented by a singleton interval and zero gradient.

Equations

• GerverSofa.Romik.SoundDual.pointConst q = { d := GerverSofa.ExactReplay.D.pointConst q n, model := GerverSofa.ScalarModel.const n ↑q, sound := ⋯ }

def GerverSofa.Romik.SoundDual.var {n : ℕ} {X : Set (Vec n)} (input : RatInterval) (k : Fin n) (h : ∀ x ∈ X, input.Contains (x k)) : SoundDual n X

A coordinate projection with its certified input interval.

Equations

• GerverSofa.Romik.SoundDual.var input k h = { d := GerverSofa.ExactReplay.D.varD input (↑k) n, model := GerverSofa.ScalarModel.var n k, sound := ⋯ }

def GerverSofa.Romik.SoundDual.add {n : ℕ} {X : Set (Vec n)} (a b : SoundDual n X) : SoundDual n X

Addition with certified interval value and gradient enclosures.

Equations

• a.add b = { d := a.d.addD b.d, model := a.model.add b.model, sound := ⋯ }

def GerverSofa.Romik.SoundDual.neg {n : ℕ} {X : Set (Vec n)} (a : SoundDual n X) : SoundDual n X

Negation with certified interval value and gradient enclosures.

Equations

• a.neg = { d := a.d.negD, model := a.model.neg, sound := ⋯ }

def GerverSofa.Romik.SoundDual.sub {n : ℕ} {X : Set (Vec n)} (a b : SoundDual n X) : SoundDual n X

Subtraction with certified interval value and gradient enclosures.

Equations

• a.sub b = { d := a.d.subD b.d, model := a.model.sub b.model, sound := ⋯ }

def GerverSofa.Romik.SoundDual.mul {n : ℕ} {X : Set (Vec n)} (a b : SoundDual n X) : SoundDual n X

Multiplication with certified interval value and gradient enclosures.

Equations

• a.mul b = { d := a.d.mulD b.d, model := a.model.mul b.model, sound := ⋯ }

def GerverSofa.Romik.SoundDual.scale {n : ℕ} {X : Set (Vec n)} (q : ℚ) (a : SoundDual n X) : SoundDual n X

Rational scaling with certified interval value and gradient enclosures.

Equations

• GerverSofa.Romik.SoundDual.scale q a = { d := GerverSofa.ExactReplay.D.scaleD q a.d, model := GerverSofa.ScalarModel.scale q a.model, sound := ⋯ }

noncomputable def GerverSofa.Romik.SoundDual.sin {n : ℕ} {X : Set (Vec n)} (a : SoundDual n X) (h : ∀ x ∈ X, 0 ≤ a.model.value x ∧ a.model.value x ≤ Real.pi / 2) : SoundDual n X

Sine with certified interval value and gradient enclosures.

Equations

• a.sin h = { d := a.d.sinD, model := a.model.sin, sound := ⋯ }

noncomputable def GerverSofa.Romik.SoundDual.cos {n : ℕ} {X : Set (Vec n)} (a : SoundDual n X) (h : ∀ x ∈ X, 0 ≤ a.model.value x ∧ a.model.value x ≤ Real.pi / 2) : SoundDual n X

Cosine with certified interval value and gradient enclosures.

Equations

• a.cos h = { d := a.d.cosD, model := a.model.cos, sound := ⋯ }

@[instance_reducible]

instance GerverSofa.Romik.SoundDual.instAdd {n : ℕ} {X : Set (Vec n)} : Add (SoundDual n X)

Equations

• GerverSofa.Romik.SoundDual.instAdd = { add := GerverSofa.Romik.SoundDual.add }

@[instance_reducible]

instance GerverSofa.Romik.SoundDual.instNeg {n : ℕ} {X : Set (Vec n)} : Neg (SoundDual n X)

Equations

• GerverSofa.Romik.SoundDual.instNeg = { neg := GerverSofa.Romik.SoundDual.neg }

@[instance_reducible]

instance GerverSofa.Romik.SoundDual.instSub {n : ℕ} {X : Set (Vec n)} : Sub (SoundDual n X)

Equations

• GerverSofa.Romik.SoundDual.instSub = { sub := GerverSofa.Romik.SoundDual.sub }

@[instance_reducible]

instance GerverSofa.Romik.SoundDual.instMul {n : ℕ} {X : Set (Vec n)} : Mul (SoundDual n X)

Equations

• GerverSofa.Romik.SoundDual.instMul = { mul := GerverSofa.Romik.SoundDual.mul }

@[instance_reducible]

instance GerverSofa.Romik.SoundDual.instHMulRat {n : ℕ} {X : Set (Vec n)} : HMul ℚ (SoundDual n X) (SoundDual n X)

Equations

• GerverSofa.Romik.SoundDual.instHMulRat = { hMul := GerverSofa.Romik.SoundDual.scale }

Small projection lemmas keep the simplifier away from the proof fields of SoundDual. All are definitional equalities.

@[simp]

theorem GerverSofa.Romik.SoundDual.const_model_value {n : ℕ} {X : Set (Vec n)} (z : RatInterval) (c : ℝ) (h : z.Contains c) (x : Vec n) : (const z c h).model.value x = c

@[simp]

theorem GerverSofa.Romik.SoundDual.pointConst_model_value {n : ℕ} {X : Set (Vec n)} (q : ℚ) (x : Vec n) : (pointConst q).model.value x = ↑q

@[simp]

theorem GerverSofa.Romik.SoundDual.var_model_value {n : ℕ} {X : Set (Vec n)} (input : RatInterval) (k : Fin n) (h : ∀ x ∈ X, input.Contains (x k)) (x : Vec n) : (var input k h).model.value x = x k

@[simp]

theorem GerverSofa.Romik.SoundDual.add_model_value {n : ℕ} {X : Set (Vec n)} (a b : SoundDual n X) (x : Vec n) : (a + b).model.value x = a.model.value x + b.model.value x

@[simp]

theorem GerverSofa.Romik.SoundDual.neg_model_value {n : ℕ} {X : Set (Vec n)} (a : SoundDual n X) (x : Vec n) : (-a).model.value x = -a.model.value x

@[simp]

theorem GerverSofa.Romik.SoundDual.sub_model_value {n : ℕ} {X : Set (Vec n)} (a b : SoundDual n X) (x : Vec n) : (a - b).model.value x = a.model.value x - b.model.value x

@[simp]

theorem GerverSofa.Romik.SoundDual.mul_model_value {n : ℕ} {X : Set (Vec n)} (a b : SoundDual n X) (x : Vec n) : (a * b).model.value x = a.model.value x * b.model.value x

@[simp]

theorem GerverSofa.Romik.SoundDual.scale_model_value {n : ℕ} {X : Set (Vec n)} (q : ℚ) (a : SoundDual n X) (x : Vec n) : (q * a).model.value x = ↑q * a.model.value x

@[simp]

theorem GerverSofa.Romik.SoundDual.sin_model_value {n : ℕ} {X : Set (Vec n)} (a : SoundDual n X) (h : ∀ x ∈ X, 0 ≤ a.model.value x ∧ a.model.value x ≤ Real.pi / 2) (x : Vec n) : (a.sin h).model.value x = Real.sin (a.model.value x)

@[simp]

theorem GerverSofa.Romik.SoundDual.cos_model_value {n : ℕ} {X : Set (Vec n)} (a : SoundDual n X) (h : ∀ x ∈ X, 0 ≤ a.model.value x ∧ a.model.value x ≤ Real.pi / 2) (x : Vec n) : (a.cos h).model.value x = Real.cos (a.model.value x)

structure GerverSofa.Romik.AngleDual (n : ℕ) (X : Set (Vec n)) : Type

A certified physical angle, used to justify every sine/cosine constructor.

• dual : SoundDual n X

  The certified scalar model for the angle variable.

• physical (x : Vec n) : x ∈ X → 0 ≤ self.dual.model.value x ∧ self.dual.model.value x ≤ Real.pi / 2

noncomputable def GerverSofa.Romik.AngleDual.sin {n : ℕ} {X : Set (Vec n)} (t : AngleDual n X) : SoundDual n X

Sine with certified interval value and gradient enclosures.

Equations

• t.sin = t.dual.sin ⋯

noncomputable def GerverSofa.Romik.AngleDual.cos {n : ℕ} {X : Set (Vec n)} (t : AngleDual n X) : SoundDual n X

Cosine with certified interval value and gradient enclosures.

Equations

• t.cos = t.dual.cos ⋯

@[simp]

theorem GerverSofa.Romik.AngleDual.sin_model_value {n : ℕ} {X : Set (Vec n)} (t : AngleDual n X) (x : Vec n) : t.sin.model.value x = Real.sin (t.dual.model.value x)

@[simp]

theorem GerverSofa.Romik.AngleDual.cos_model_value {n : ℕ} {X : Set (Vec n)} (t : AngleDual n X) (x : Vec n) : t.cos.model.value x = Real.cos (t.dual.model.value x)

structure GerverSofa.Romik.FullVars (X : Set (Vec 22)) : Type

Named proof-carrying versions of all direct-system variables.

• k11 : SoundDual 22 X

  Horizontal translation coefficient for phase 1 as a certified dual interval.

• k12 : SoundDual 22 X

  Vertical translation coefficient for phase 1 as a certified dual interval.

• k21 : SoundDual 22 X

  Horizontal translation coefficient for phase 2 as a certified dual interval.

• k22 : SoundDual 22 X

  Vertical translation coefficient for phase 2 as a certified dual interval.

• k31 : SoundDual 22 X

  Horizontal translation coefficient for phase 3 as a certified dual interval.

• k32 : SoundDual 22 X

  Vertical translation coefficient for phase 3 as a certified dual interval.

• k41 : SoundDual 22 X

  Horizontal translation coefficient for phase 4 as a certified dual interval.

• k42 : SoundDual 22 X

  Vertical translation coefficient for phase 4 as a certified dual interval.

• k51 : SoundDual 22 X

  Horizontal translation coefficient for phase 5 as a certified dual interval.

• k52 : SoundDual 22 X

  Vertical translation coefficient for phase 5 as a certified dual interval.

• a1 : SoundDual 22 X

  Coefficient 1 in the phase 1 closed formula as a certified dual interval.

• a2 : SoundDual 22 X

  Coefficient 2 in the phase 1 closed formula as a certified dual interval.

• b1 : SoundDual 22 X

  Coefficient 1 in the phase 2 closed formula as a certified dual interval.

• b2 : SoundDual 22 X

  Coefficient 2 in the phase 2 closed formula as a certified dual interval.

• c1 : SoundDual 22 X

  Coefficient 1 in the phase 3 closed formula as a certified dual interval.

• c2 : SoundDual 22 X

  Coefficient 2 in the phase 3 closed formula as a certified dual interval.

• d1 : SoundDual 22 X

  Coefficient 1 in the phase 4 closed formula as a certified dual interval.

• d2 : SoundDual 22 X

  Coefficient 2 in the phase 4 closed formula as a certified dual interval.

• e1 : SoundDual 22 X

  Coefficient 1 in the phase 5 closed formula as a certified dual interval.

• e2 : SoundDual 22 X

  Coefficient 2 in the phase 5 closed formula as a certified dual interval.

def GerverSofa.Romik.inputDual (i : Fin 22) : SoundDual 22 vectorBox

The 22 coordinate variables equipped with their input-enclosure proofs.

Equations

• GerverSofa.Romik.inputDual i = GerverSofa.Romik.SoundDual.var (GerverSofa.ExactReplay.getI GerverSofa.ExactReplay.fullInputBox ↑i) i ⋯

@[simp]

theorem GerverSofa.Romik.inputDual_model_value (i : Fin 22) (x : Vec 22) : (inputDual i).model.value x = x i

def GerverSofa.Romik.fullVars : FullVars vectorBox

Named first twenty variables in verifier order.

Equations

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

noncomputable def GerverSofa.Romik.piDual : SoundDual 22 vectorBox

Exact proof-carrying π constant.

Equations

• GerverSofa.Romik.piDual = GerverSofa.Romik.SoundDual.const GerverSofa.ExactReplay.piI Real.pi GerverSofa.ExactReplay.piI_contains_pi

@[simp]

theorem GerverSofa.Romik.piDual_model_value (x : Vec 22) : piDual.model.value x = Real.pi

def GerverSofa.Romik.phiDual : AngleDual 22 vectorBox

First switching angle.

Equations

• GerverSofa.Romik.phiDual = { dual := GerverSofa.Romik.inputDual 20, physical := GerverSofa.Romik.phiDual._proof_1 }

@[simp]

theorem GerverSofa.Romik.phiDual_model_value (x : Vec 22) : phiDual.dual.model.value x = x 20

def GerverSofa.Romik.thetaDual : AngleDual 22 vectorBox

Second switching angle.

Equations

• GerverSofa.Romik.thetaDual = { dual := GerverSofa.Romik.inputDual 21, physical := GerverSofa.Romik.thetaDual._proof_1 }

@[simp]

theorem GerverSofa.Romik.thetaDual_model_value (x : Vec 22) : thetaDual.dual.model.value x = x 21

noncomputable def GerverSofa.Romik.etaDual : AngleDual 22 vectorBox

Reflected third switching angle π/2-θ.

Equations

• GerverSofa.Romik.etaDual = { dual := 1 / 2 * GerverSofa.Romik.piDual - GerverSofa.Romik.thetaDual.dual, physical := GerverSofa.Romik.etaDual._proof_1 }

@[simp]

theorem GerverSofa.Romik.etaDual_model_value (x : Vec 22) : etaDual.dual.model.value x = Real.pi / 2 - x 21

noncomputable def GerverSofa.Romik.tauDual : AngleDual 22 vectorBox

Reflected fourth switching angle π/2-φ.

Equations

• GerverSofa.Romik.tauDual = { dual := 1 / 2 * GerverSofa.Romik.piDual - GerverSofa.Romik.phiDual.dual, physical := GerverSofa.Romik.tauDual._proof_1 }

@[simp]

theorem GerverSofa.Romik.tauDual_model_value (x : Vec 22) : tauDual.dual.model.value x = Real.pi / 2 - x 20

noncomputable def GerverSofa.Romik.rotDual (t : AngleDual 22 vectorBox) (z1 z2 : SoundDual 22 vectorBox) : SoundDual 22 vectorBox × SoundDual 22 vectorBox

Rotation of a proof-carrying body-frame vector.

Equations

• GerverSofa.Romik.rotDual t z1 z2 = (t.cos * z1 - t.sin * z2, t.sin * z1 + t.cos * z2)

noncomputable def GerverSofa.Romik.pathPieceDual (j : ℕ) (t : AngleDual 22 vectorBox) (p : FullVars vectorBox := fullVars) : SoundDual 22 vectorBox × SoundDual 22 vectorBox

One proof-carrying path piece.

Equations

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

noncomputable def GerverSofa.Romik.alphaBetaDual (j : ℕ) (t : AngleDual 22 vectorBox) (p : FullVars vectorBox := fullVars) : SoundDual 22 vectorBox × SoundDual 22 vectorBox

Body-frame derivative coefficients for one phase.

Equations

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

noncomputable def GerverSofa.Romik.pathPrimeDual (j : ℕ) (t : AngleDual 22 vectorBox) (p : FullVars vectorBox := fullVars) : SoundDual 22 vectorBox × SoundDual 22 vectorBox

World-frame derivative piece.

Equations

• GerverSofa.Romik.pathPrimeDual j t p = GerverSofa.Romik.rotDual t (GerverSofa.Romik.alphaBetaDual j t p).1 (GerverSofa.Romik.alphaBetaDual j t p).2

noncomputable def GerverSofa.Romik.fullDualOutput : List (SoundDual 22 vectorBox)

The complete proof-carrying direct system in manuscript order.

Equations

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

Public-shape unfold lemmas for the three derivative path pieces.

Systems.lean deliberately hides the helper pathPrimeFromAB. When system is unfolded outside that file, the private helper survives as an inaccessible constant, so ring cannot see that the right-hand side is just a rotation. These rfl lemmas expose exactly the public normal form needed by the four derivative-matching equations.

The semantic identification is split coordinatewise so each normalization gets its own heartbeat budget. A single 22-way fin_cases <;> simp <;> ring command is mathematically fine but deterministically exhausts 200000 heartbeats.

theorem GerverSofa.Romik.fullDualOutput_model_eq (x : Vec 22) : (fun (i : Fin 22) => (fullDualOutput.getD (↑i) (SoundDual.pointConst 0)).model.value x) = vectorSystem x

The real models carried by fullDualOutput are exactly the 22 manuscript functions in finite-vector coordinates.

Gerver sofa dependency batch

• KernelOnly.PartF.F01AffineOrder.
• KernelOnly.PartF.F01PhaseAlgebra.
• KernelOnly.PartF.F01SetMotion.
• KernelOnly.PartF.F02Coordinates.
• KernelOnly.PartF.F04IntegralPrimitives.
• KernelOnly.PartF.F04IntegralEvaluation.
• KernelOnly.PartF.F05DictionaryEquations.
• KernelOnly.PartF.F06ReverseSystem.
• KernelOnly.PartF.F06FullReconstruction.

F01: the affine-order bridge for issue #5270

The two constructors are deliberately given different names. No upstream definition is changed or imported, and no theorem from the conjecture file is used. Both application conventions and the conversion between them are proved for an arbitrary linear isometry equivalence.

@[reducible, inline]

abbrev GerverSofa.PartF.Plane : Type

The Euclidean plane used for the continuous rigid-motion formulation.

Equations

• GerverSofa.PartF.Plane = EuclideanSpace ℝ (Fin 2)

@[reducible, inline]

abbrev GerverSofa.PartF.Rigid : Type

Affine isometries of the Euclidean plane.

Equations

• GerverSofa.PartF.Rigid = (GerverSofa.PartF.Plane ≃ᵃⁱ[ℝ] GerverSofa.PartF.Plane)

@[instance_reducible]

noncomputable instance GerverSofa.PartF.planeOriented : Module.Oriented ℝ Plane (Fin 2)

The ordered coordinate-basis orientation used by the pinned upstream FormalConjecturesForMathlib/Geometry/2d.lean. Importing Mathlib alone does not install that project's plane-orientation instance.

Equations

• GerverSofa.PartF.planeOriented = { positiveOrientation := (PiLp.basisFun 2 ℝ (Fin 2)).orientation }

instance GerverSofa.PartF.planeFactFinrank : Fact (Module.finrank ℝ Plane = 2)

The second instance supplied by the same upstream plane helper.

@[instance_reducible]

noncomputable instance GerverSofa.PartF.rigidTopology : TopologicalSpace Rigid

The topology used by the pinned MovingSofa.IsMovingSofa definition.

Equations

• GerverSofa.PartF.rigidTopology = TopologicalSpace.induced (fun (e : GerverSofa.PartF.Rigid) => (AffineIsometryEquiv.toAffineIsometry e).toContinuousAffineMap) inferInstance

noncomputable def GerverSofa.PartF.rotateThenTranslate (R : Plane ≃ₗᵢ[ℝ] Plane) (p : Plane) : Rigid

The composition currently implemented upstream: q ↦ R q + p.

Equations

• GerverSofa.PartF.rotateThenTranslate R p = R.toAffineIsometryEquiv.trans (AffineIsometryEquiv.vaddConst ℝ p)

noncomputable def GerverSofa.PartF.translateThenRotate (R : Plane ≃ₗᵢ[ℝ] Plane) (p : Plane) : Rigid

The documented composition: q ↦ R (q + p).

Equations

• GerverSofa.PartF.translateThenRotate R p = (AffineIsometryEquiv.vaddConst ℝ p).trans R.toAffineIsometryEquiv

@[simp]

theorem GerverSofa.PartF.rotateThenTranslate_apply (R : Plane ≃ₗᵢ[ℝ] Plane) (p q : Plane) : (rotateThenTranslate R p) q = R q + p

@[simp]

theorem GerverSofa.PartF.translateThenRotate_apply (R : Plane ≃ₗᵢ[ℝ] Plane) (p q : Plane) : (translateThenRotate R p) q = R (q + p)

theorem GerverSofa.PartF.translateThenRotate_eq_rotateThenTranslate (R : Plane ≃ₗᵢ[ℝ] Plane) (p : Plane) : translateThenRotate R p = rotateThenTranslate R (R p)

Keeping the old composition is equivalent to rotating the translation.

noncomputable def GerverSofa.PartF.rotation (t : ℝ) : Plane ≃ₗᵢ[ℝ] Plane

Counterclockwise rotation of the oriented plane through angle t.

Equations

• GerverSofa.PartF.rotation t = EuclideanGeometry.o.rotation ↑t

noncomputable def GerverSofa.PartF.bodyFrame (t : ℝ) (p : Plane) : Rigid

Translate by the body-frame offset and then rotate through t.

Equations

• GerverSofa.PartF.bodyFrame t p = GerverSofa.PartF.translateThenRotate (GerverSofa.PartF.rotation t) p

noncomputable def GerverSofa.PartF.worldFrame (t : ℝ) (x : Plane) : Rigid

Rotate through t and then translate by the world position.

Equations

• GerverSofa.PartF.worldFrame t x = GerverSofa.PartF.rotateThenTranslate (GerverSofa.PartF.rotation t) x

theorem GerverSofa.PartF.bodyFrame_eq_worldFrame (t : ℝ) (p : Plane) : bodyFrame t p = worldFrame t ((rotation t) p)

F01: algebraic half of the integral-to-five-phase representation

The coefficient dictionary and the five explicit body-frame branches come from the 4 September integral-motion excerpt. They are compared to the actual Romik.path1 ... Romik.path5 definitions, then assembled using the same if boundaries as Romik.path.

This module does NOT evaluate the integrals: closedPath is explicitly named as a closed-form candidate. Proving that the pinned integral path equals it, and identifying dictionary d with the certified 22D tuple, remain separate obligations. No such equality is assumed here.

noncomputable def GerverSofa.PartF.Phases.T : ℝ

The terminal rotation angle π/2.

Equations

• GerverSofa.PartF.Phases.T = Real.pi / 2

noncomputable def GerverSofa.PartF.Phases.hStar (d : Reduced.Params) : ℝ

The auxiliary height parameter (a + θ - φ - 1) / 2.

Equations

• GerverSofa.PartF.Phases.hStar d = (d.a + d.theta - d.phi - 1) / 2

noncomputable def GerverSofa.PartF.Phases.U4 (d : Reduced.Params) : ℝ

Phase 4 integration constant for the vertical primitive.

Equations

• GerverSofa.PartF.Phases.U4 d = (1 + d.a) / 2 * Real.cos d.phi - (d.b + 1 / 2) * Real.sin d.phi

noncomputable def GerverSofa.PartF.Phases.V4 (d : Reduced.Params) : ℝ

Phase 4 integration constant for the horizontal primitive.

Equations

• GerverSofa.PartF.Phases.V4 d = 1 - (d.b + 1 / 2) * Real.cos d.phi - (1 + d.a) / 2 * Real.sin d.phi

noncomputable def GerverSofa.PartF.Phases.U3 (d : Reduced.Params) : ℝ

Phase 3 integration constant for the vertical primitive.

Equations

• GerverSofa.PartF.Phases.U3 d = GerverSofa.PartF.Phases.U4 d + 1 / 2 * Real.sin d.theta - GerverSofa.PartF.Phases.hStar d * Real.cos d.theta

noncomputable def GerverSofa.PartF.Phases.V3 (d : Reduced.Params) : ℝ

Phase 3 integration constant for the horizontal primitive.

Equations

• GerverSofa.PartF.Phases.V3 d = GerverSofa.PartF.Phases.V4 d + 1 / 2 * Real.cos d.theta + GerverSofa.PartF.Phases.hStar d * Real.sin d.theta

noncomputable def GerverSofa.PartF.Phases.U2 (d : Reduced.Params) : ℝ

Phase 2 integration constant for the vertical primitive.

Equations

• GerverSofa.PartF.Phases.U2 d = GerverSofa.PartF.Phases.U4 d

noncomputable def GerverSofa.PartF.Phases.V2 (d : Reduced.Params) : ℝ

Phase 2 integration constant for the horizontal primitive.

Equations

• GerverSofa.PartF.Phases.V2 d = GerverSofa.PartF.Phases.V4 d + Real.cos d.theta + 2 * GerverSofa.PartF.Phases.hStar d * Real.sin d.theta

noncomputable def GerverSofa.PartF.Phases.U1 (d : Reduced.Params) : ℝ

Phase 1 integration constant for the vertical primitive.

Equations

• GerverSofa.PartF.Phases.U1 d = GerverSofa.PartF.Phases.U2 d + d.a / 2 * Real.cos d.phi - 1 / 2 * Real.sin d.phi

noncomputable def GerverSofa.PartF.Phases.V1 (d : Reduced.Params) : ℝ

Phase 1 integration constant for the horizontal primitive.

Equations

• GerverSofa.PartF.Phases.V1 d = GerverSofa.PartF.Phases.V2 d + d.a / 2 * Real.sin d.phi + 1 / 2 * Real.cos d.phi

noncomputable def GerverSofa.PartF.Phases.ell (d : Reduced.Params) : ℝ

The first-phase offset determined by 4 V1 - 2.

Equations

• GerverSofa.PartF.Phases.ell d = 4 * GerverSofa.PartF.Phases.V1 d - 2

theorem GerverSofa.PartF.Phases.U1_eq_half (d : Reduced.Params) (hd : Reduced.Equations d) : U1 d = 1 / 2

theorem GerverSofa.PartF.Phases.ell_eq (d : Reduced.Params) (hd : Reduced.Equations d) : ell d = V2 d + V4 d

theorem GerverSofa.PartF.Phases.ell_eq_two_V3 (d : Reduced.Params) (hd : Reduced.Equations d) : ell d = 2 * V3 d

noncomputable def GerverSofa.PartF.Phases.dictionary (d : Reduced.Params) : Romik.Params

Express all twenty-two Romik parameters in terms of the four reduced parameters.

Equations

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

@[simp]

theorem GerverSofa.PartF.Phases.dictionary_phi (d : Reduced.Params) : (dictionary d).phi = d.phi

@[simp]

theorem GerverSofa.PartF.Phases.dictionary_theta (d : Reduced.Params) : (dictionary d).theta = d.theta

noncomputable def GerverSofa.PartF.Phases.g2 (d : Reduced.Params) (t : ℝ) : ℝ

The polynomial profile for phase 2 of the path.

Equations

• GerverSofa.PartF.Phases.g2 d t = (1 + d.a + t - d.phi) / 2

def GerverSofa.PartF.Phases.g3 (d : Reduced.Params) (t : ℝ) : ℝ

The polynomial profile for phase 3 of the path.

Equations

• GerverSofa.PartF.Phases.g3 d t = d.a + t - d.phi

noncomputable def GerverSofa.PartF.Phases.g4 (d : Reduced.Params) (t : ℝ) : ℝ

The polynomial profile for phase 4 of the path.

Equations

• GerverSofa.PartF.Phases.g4 d t = d.b + 1 / 2 - (GerverSofa.PartF.Phases.T - d.phi - t) * (1 + d.a) / 2 - (GerverSofa.PartF.Phases.T - d.phi - t) ^ 2 / 4

noncomputable def GerverSofa.PartF.Phases.closed1 (d : Reduced.Params) (t : ℝ) : Point

The closed rotation-path formula for phase 1.

Equations

• GerverSofa.PartF.Phases.closed1 d t = (Real.cos t - 1, -1 / 2 + 1 / 2 * Real.cos t + (GerverSofa.PartF.Phases.V1 d - GerverSofa.PartF.Phases.ell d) * Real.sin t)

noncomputable def GerverSofa.PartF.Phases.closed2 (d : Reduced.Params) (t : ℝ) : Point

The closed rotation-path formula for phase 2.

Equations

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

noncomputable def GerverSofa.PartF.Phases.closed3 (d : Reduced.Params) (t : ℝ) : Point

The closed rotation-path formula for phase 3.

Equations

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

noncomputable def GerverSofa.PartF.Phases.closed4 (d : Reduced.Params) (t : ℝ) : Point

The closed rotation-path formula for phase 4.

Equations

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

noncomputable def GerverSofa.PartF.Phases.closed5 (d : Reduced.Params) (t : ℝ) : Point

The closed rotation-path formula for phase 5.

Equations

• GerverSofa.PartF.Phases.closed5 d t = (-1 / 2 + GerverSofa.PartF.Phases.V1 d * Real.cos t + 1 / 2 * Real.sin t, (1 - GerverSofa.PartF.Phases.ell d) * Real.sin t - 1)

theorem GerverSofa.PartF.Phases.phase1 (d : Reduced.Params) (t : ℝ) : Romik.rot t (closed1 d t) = Romik.path1 (dictionary d) t

theorem GerverSofa.PartF.Phases.phase2 (d : Reduced.Params) (hd : Reduced.Equations d) (t : ℝ) : Romik.rot t (closed2 d t) = Romik.path2 (dictionary d) t

theorem GerverSofa.PartF.Phases.phase3 (d : Reduced.Params) (hd : Reduced.Equations d) (t : ℝ) : Romik.rot t (closed3 d t) = Romik.path3 (dictionary d) t

theorem GerverSofa.PartF.Phases.phase4 (d : Reduced.Params) (hd : Reduced.Equations d) (t : ℝ) : Romik.rot t (closed4 d t) = Romik.path4 (dictionary d) t

theorem GerverSofa.PartF.Phases.phase5 (d : Reduced.Params) (t : ℝ) : Romik.rot t (closed5 d t) = Romik.path5 (dictionary d) t

noncomputable def GerverSofa.PartF.Phases.closedPath (d : Reduced.Params) (t : ℝ) : Point

The five-branch closed formula for the rotation path.

Equations

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

theorem GerverSofa.PartF.Phases.fivePhaseRepresentation (d : Reduced.Params) (hd : Reduced.Equations d) (t : ℝ) : Romik.rot t (closedPath d t) = Romik.path (dictionary d) t

Exact assembly for the explicit closed path, including every switching endpoint. This is not yet the corresponding theorem for the integral path.

F01: supporting intersections and their continuous inverse motion

Model.IsMovingSofa has the seven fields and the rigid-motion topology of the upstream definition. This local, independently named model avoids importing upstream conjectures with unfinished proof terms. Its concrete instantiation for the integral Gerver path still needs the analytic bridge.

def GerverSofa.PartF.frameIntersection (F : ↑unitInterval → Rigid) (H V L : Set Plane) : Set Plane

Intersect the endpoint hallway arms and all intermediate moving hallways.

Equations

• GerverSofa.PartF.frameIntersection F H V L = ⇑(F 0) '' H ∩ ⇑(F 1) '' V ∩ ⋂ (s : ↑unitInterval), ⇑(F s) '' L

def GerverSofa.PartF.angleIntersection (F : ℝ → Rigid) (H V L : Set Plane) : Set Plane

The hallway intersection parametrized by angles from zero to π/2.

Equations

• GerverSofa.PartF.angleIntersection F H V L = ⇑(F 0) '' H ∩ ⇑(F (Real.pi / 2)) '' V ∩ ⋂ t ∈ Set.Icc 0 (Real.pi / 2), ⇑(F t) '' L

def GerverSofa.PartF.bodySofa (p : ℝ → Plane) (H V L : Set Plane) : Set Plane

The hallway intersection generated by a path in body-frame coordinates.

Equations

• GerverSofa.PartF.bodySofa p H V L = GerverSofa.PartF.angleIntersection (fun (t : ℝ) => GerverSofa.PartF.bodyFrame t (p t)) H V L

def GerverSofa.PartF.worldSofa (x : ℝ → Plane) (H V L : Set Plane) : Set Plane

The hallway intersection generated by a path in world-frame coordinates.

Equations

• GerverSofa.PartF.worldSofa x H V L = GerverSofa.PartF.angleIntersection (fun (t : ℝ) => GerverSofa.PartF.worldFrame t (x t)) H V L

theorem GerverSofa.PartF.bodySofa_eq_worldSofa_of_path_identity (p x : ℝ → Plane) (H V L : Set Plane) (hpath : ∀ t ∈ Set.Icc 0 (Real.pi / 2), x t = (rotation t) (p t)) : bodySofa p H V L = worldSofa x H V L

theorem GerverSofa.PartF.angleIntersection_eq_frameIntersection (F : ℝ → Rigid) (H V L : Set Plane) : angleIntersection F H V L = frameIntersection (fun (s : ↑unitInterval) => F (↑s * (Real.pi / 2))) H V L

Normalizing the physical angle does not change the intersection.

def GerverSofa.PartF.Model.horizontalHallway : Set Plane

The horizontal unit-width hallway arm extending to the left.

Equations

• GerverSofa.PartF.Model.horizontalHallway = {q : GerverSofa.PartF.Plane | q.ofLp 0 ≤ 1 ∧ 0 ≤ q.ofLp 1 ∧ q.ofLp 1 ≤ 1}

def GerverSofa.PartF.Model.verticalHallway : Set Plane

The vertical unit-width hallway arm extending downwards.

Equations

• GerverSofa.PartF.Model.verticalHallway = {q : GerverSofa.PartF.Plane | 0 ≤ q.ofLp 0 ∧ q.ofLp 0 ≤ 1 ∧ q.ofLp 1 ≤ 1}

def GerverSofa.PartF.Model.hallway : Set Plane

The union of the two perpendicular unit-width hallway arms.

Equations

• GerverSofa.PartF.Model.hallway = GerverSofa.PartF.Model.horizontalHallway ∪ GerverSofa.PartF.Model.verticalHallway

structure GerverSofa.PartF.Model.IsMovingSofa (S : Set Plane) (m : ↑unitInterval → Rigid) : Prop

A nonempty closed connected set moving continuously between the hallway arms.

• isConnected : IsConnected S
• isClosed : IsClosed S
• continuous : Continuous m
• zero : m 0 = AffineIsometryEquiv.refl ℝ Plane
• initial : S ⊆ horizontalHallway
• subset_hallway (s : ↑unitInterval) : ⇑(m s) '' S ⊆ hallway
• final : ⇑(m 1) '' S ⊆ verticalHallway

F02: the coordinate homeomorphism

The product Point = ℝ × ℝ and Plane = EuclideanSpace ℝ (Fin 2) have the same coordinates and topology. Their norms differ. Accordingly, the coordinate identification below is a linear equivalence and a homeomorphism. Euclidean isometries are constructed separately.

def GerverSofa.PartF.Coordinates.toPlane (q : Point) : Plane

Convert a pair of real coordinates to a Euclidean vector.

Equations

• GerverSofa.PartF.Coordinates.toPlane q = !₂[q.1, q.2]

def GerverSofa.PartF.Coordinates.fromPlane (q : Plane) : Point

Extract the two real coordinates of a Euclidean vector.

Equations

• GerverSofa.PartF.Coordinates.fromPlane q = (q.ofLp 0, q.ofLp 1)

@[simp]

theorem GerverSofa.PartF.Coordinates.toPlane_zero_coord (q : Point) : (toPlane q).ofLp 0 = q.1

@[simp]

theorem GerverSofa.PartF.Coordinates.toPlane_one_coord (q : Point) : (toPlane q).ofLp 1 = q.2

theorem GerverSofa.PartF.Coordinates.plane_ext {q r : Plane} (h0 : q.ofLp 0 = r.ofLp 0) (h1 : q.ofLp 1 = r.ofLp 1) : q = r

@[simp]

theorem GerverSofa.PartF.Coordinates.fromPlane_toPlane (q : Point) : fromPlane (toPlane q) = q

@[simp]

theorem GerverSofa.PartF.Coordinates.toPlane_fromPlane (q : Plane) : toPlane (fromPlane q) = q

theorem GerverSofa.PartF.Coordinates.toPlane_add (q r : Point) : toPlane (q + r) = toPlane q + toPlane r

theorem GerverSofa.PartF.Coordinates.toPlane_smul (c : ℝ) (q : Point) : toPlane (c • q) = c • toPlane q

def GerverSofa.PartF.Coordinates.linearEquiv : Point ≃ₗ[ℝ] Plane

The coordinate equivalence, without any assertion that the two norms agree.

Equations

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

noncomputable def GerverSofa.PartF.Coordinates.homeomorph : Point ≃ₜ Plane

The coordinate homeomorphism between real pairs and the Euclidean plane.

Equations

• GerverSofa.PartF.Coordinates.homeomorph = GerverSofa.PartF.Coordinates.linearEquiv.toContinuousLinearEquiv.toHomeomorph

theorem GerverSofa.PartF.Coordinates.continuous_toPlane : Continuous toPlane

theorem GerverSofa.PartF.Coordinates.continuous_fromPlane : Continuous fromPlane

theorem GerverSofa.PartF.Coordinates.image_eq_preimage (S : Set Point) : toPlane '' S = fromPlane ⁻¹' S

theorem GerverSofa.PartF.Coordinates.isClosed_image {S : Set Point} (hS : IsClosed S) : IsClosed (toPlane '' S)

theorem GerverSofa.PartF.Coordinates.isConnected_image {S : Set Point} (hS : IsConnected S) : IsConnected (toPlane '' S)

theorem GerverSofa.PartF.Coordinates.horizontal_image : toPlane '' horizontalArm = Model.horizontalHallway

theorem GerverSofa.PartF.Coordinates.vertical_image : toPlane '' verticalArm = Model.verticalHallway

theorem GerverSofa.PartF.Coordinates.hallway_image : toPlane '' hallway = Model.hallway

F04: literal integral data and its branch primitives

The parameterized definitions below are the pinned upstream scalar integrals. The phase boundaries are preserved. Integrating across the jumps will use equality on open intervals, not an incorrect global continuity assertion for r.

noncomputable def GerverSofa.PartF.Integrals.eta (d : Reduced.Params) : ℝ

The reflected second switching angle π/2 - θ.

Equations

• GerverSofa.PartF.Integrals.eta d = GerverSofa.PartF.Phases.T - d.theta

noncomputable def GerverSofa.PartF.Integrals.tau (d : Reduced.Params) : ℝ

The reflected first switching angle π/2 - φ.

Equations

• GerverSofa.PartF.Integrals.tau d = GerverSofa.PartF.Phases.T - d.phi

def GerverSofa.PartF.Integrals.Ordered (d : Reduced.Params) : Prop

The switching-angle condition 0 ≤ φ ≤ θ ≤ π/4.

Equations

• GerverSofa.PartF.Integrals.Ordered d = (0 ≤ d.phi ∧ d.phi ≤ d.theta ∧ d.theta ≤ Real.pi / 4)

theorem GerverSofa.PartF.Integrals.ordered_knots (d : Reduced.Params) (ho : Ordered d) : 0 ≤ d.phi ∧ d.phi ≤ d.theta ∧ d.theta ≤ eta d ∧ eta d ≤ tau d ∧ tau d ≤ Phases.T

noncomputable def GerverSofa.PartF.Integrals.r1 (_d : Reduced.Params) (_t : ℝ) : ℝ

The integrand profile on phase 1.

Equations

• GerverSofa.PartF.Integrals.r1 _d _t = 1 / 2

noncomputable def GerverSofa.PartF.Integrals.r2 (d : Reduced.Params) (t : ℝ) : ℝ

The integrand profile on phase 2.

Equations

• GerverSofa.PartF.Integrals.r2 d t = GerverSofa.PartF.Phases.g2 d t

def GerverSofa.PartF.Integrals.r3 (d : Reduced.Params) (t : ℝ) : ℝ

The integrand profile on phase 3.

Equations

• GerverSofa.PartF.Integrals.r3 d t = GerverSofa.PartF.Phases.g3 d t

noncomputable def GerverSofa.PartF.Integrals.r4 (d : Reduced.Params) (t : ℝ) : ℝ

The integrand profile on phase 4.

Equations

• GerverSofa.PartF.Integrals.r4 d t = d.b - (GerverSofa.PartF.Phases.T - t - d.phi) * (1 + d.a) / 2 - (GerverSofa.PartF.Phases.T - t - d.phi) ^ 2 / 4

noncomputable def GerverSofa.PartF.Integrals.r (d : Reduced.Params) (t : ℝ) : ℝ

The piecewise phase profile used in the integral representation.

Equations

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

noncomputable def GerverSofa.PartF.Integrals.xi (d : Reduced.Params) (t : ℝ) : ℝ

One minus the cosine-weighted profile integral from t to the last switching angle.

Equations

• GerverSofa.PartF.Integrals.xi d t = 1 - ∫ (s : ℝ) in t..GerverSofa.PartF.Integrals.tau d, GerverSofa.PartF.Integrals.r d s * Real.cos s

noncomputable def GerverSofa.PartF.Integrals.zeta (d : Reduced.Params) (t : ℝ) : ℝ

The sine-weighted profile integral from t to the last switching angle.

Equations

• GerverSofa.PartF.Integrals.zeta d t = ∫ (s : ℝ) in t..GerverSofa.PartF.Integrals.tau d, GerverSofa.PartF.Integrals.r d s * Real.sin s

noncomputable def GerverSofa.PartF.Integrals.path (d : Reduced.Params) (t : ℝ) : Point

The rotation path expressed using the two profile integrals.

Equations

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

noncomputable def GerverSofa.PartF.Integrals.dg4 (d : Reduced.Params) (t : ℝ) : ℝ

The derivative formula for the fourth phase profile.

Equations

• GerverSofa.PartF.Integrals.dg4 d t = (1 + d.a) / 2 + (GerverSofa.PartF.Phases.T - d.phi - t) / 2

noncomputable def GerverSofa.PartF.Integrals.primitiveX (V : ℝ) (g gp : ℝ → ℝ) (t : ℝ) : ℝ

The horizontal primitive assembled from a profile, its derivative, and an offset.

Equations

• GerverSofa.PartF.Integrals.primitiveX V g gp t = V + g t * Real.sin t + gp t * Real.cos t

noncomputable def GerverSofa.PartF.Integrals.primitiveY (U : ℝ) (g gp : ℝ → ℝ) (t : ℝ) : ℝ

The vertical primitive assembled from a profile, its derivative, and an offset.

Equations

• GerverSofa.PartF.Integrals.primitiveY U g gp t = U + g t * Real.cos t - gp t * Real.sin t

noncomputable def GerverSofa.PartF.Integrals.X1 (d : Reduced.Params) : ℝ → ℝ

Horizontal primitive specialized to phase 1.

Equations

• GerverSofa.PartF.Integrals.X1 d = GerverSofa.PartF.Integrals.primitiveX (GerverSofa.PartF.Phases.V1 d) (GerverSofa.PartF.Integrals.r1 d) fun (x : ℝ) => 0

noncomputable def GerverSofa.PartF.Integrals.Y1 (d : Reduced.Params) : ℝ → ℝ

Vertical primitive specialized to phase 1.

Equations

• GerverSofa.PartF.Integrals.Y1 d = GerverSofa.PartF.Integrals.primitiveY (GerverSofa.PartF.Phases.U1 d) (GerverSofa.PartF.Integrals.r1 d) fun (x : ℝ) => 0

noncomputable def GerverSofa.PartF.Integrals.X2 (d : Reduced.Params) : ℝ → ℝ

Horizontal primitive specialized to phase 2.

Equations

• GerverSofa.PartF.Integrals.X2 d = GerverSofa.PartF.Integrals.primitiveX (GerverSofa.PartF.Phases.V2 d) (GerverSofa.PartF.Phases.g2 d) fun (x : ℝ) => 1 / 2

noncomputable def GerverSofa.PartF.Integrals.Y2 (d : Reduced.Params) : ℝ → ℝ

Vertical primitive specialized to phase 2.

Equations

• GerverSofa.PartF.Integrals.Y2 d = GerverSofa.PartF.Integrals.primitiveY (GerverSofa.PartF.Phases.U2 d) (GerverSofa.PartF.Phases.g2 d) fun (x : ℝ) => 1 / 2

noncomputable def GerverSofa.PartF.Integrals.X3 (d : Reduced.Params) : ℝ → ℝ

Horizontal primitive specialized to phase 3.

Equations

• GerverSofa.PartF.Integrals.X3 d = GerverSofa.PartF.Integrals.primitiveX (GerverSofa.PartF.Phases.V3 d) (GerverSofa.PartF.Phases.g3 d) fun (x : ℝ) => 1

noncomputable def GerverSofa.PartF.Integrals.Y3 (d : Reduced.Params) : ℝ → ℝ

Vertical primitive specialized to phase 3.

Equations

• GerverSofa.PartF.Integrals.Y3 d = GerverSofa.PartF.Integrals.primitiveY (GerverSofa.PartF.Phases.U3 d) (GerverSofa.PartF.Phases.g3 d) fun (x : ℝ) => 1

noncomputable def GerverSofa.PartF.Integrals.X4 (d : Reduced.Params) : ℝ → ℝ

Horizontal primitive specialized to phase 4.

Equations

• GerverSofa.PartF.Integrals.X4 d = GerverSofa.PartF.Integrals.primitiveX (GerverSofa.PartF.Phases.V4 d) (GerverSofa.PartF.Phases.g4 d) (GerverSofa.PartF.Integrals.dg4 d)

noncomputable def GerverSofa.PartF.Integrals.Y4 (d : Reduced.Params) : ℝ → ℝ

Vertical primitive specialized to phase 4.

Equations

• GerverSofa.PartF.Integrals.Y4 d = GerverSofa.PartF.Integrals.primitiveY (GerverSofa.PartF.Phases.U4 d) (GerverSofa.PartF.Phases.g4 d) (GerverSofa.PartF.Integrals.dg4 d)

theorem GerverSofa.PartF.Integrals.primitiveX_hasDerivAt (V : ℝ) {g gp : ℝ → ℝ} {t gpp : ℝ} (hg : HasDerivAt g (gp t) t) (hgp : HasDerivAt gp gpp t) : HasDerivAt (primitiveX V g gp) ((g t + gpp) * Real.cos t) t

F05 repair: normalize only the scalar derivative, never typeclass arguments.

theorem GerverSofa.PartF.Integrals.primitiveY_hasDerivAt (U : ℝ) {g gp : ℝ → ℝ} {t gpp : ℝ} (hg : HasDerivAt g (gp t) t) (hgp : HasDerivAt gp gpp t) : HasDerivAt (primitiveY U g gp) (-(g t + gpp) * Real.sin t) t

theorem GerverSofa.PartF.Integrals.g2_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Phases.g2 d) (1 / 2) t

theorem GerverSofa.PartF.Integrals.g3_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Phases.g3 d) 1 t

theorem GerverSofa.PartF.Integrals.g4_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Phases.g4 d) (dg4 d t) t

theorem GerverSofa.PartF.Integrals.dg4_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (dg4 d) (-1 / 2) t

theorem GerverSofa.PartF.Integrals.X1_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (X1 d) (r1 d t * Real.cos t) t

theorem GerverSofa.PartF.Integrals.Y1_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Y1 d) (-r1 d t * Real.sin t) t

theorem GerverSofa.PartF.Integrals.X2_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (X2 d) (r2 d t * Real.cos t) t

theorem GerverSofa.PartF.Integrals.Y2_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Y2 d) (-r2 d t * Real.sin t) t

theorem GerverSofa.PartF.Integrals.X3_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (X3 d) (r3 d t * Real.cos t) t

theorem GerverSofa.PartF.Integrals.Y3_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Y3 d) (-r3 d t * Real.sin t) t

theorem GerverSofa.PartF.Integrals.X4_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (X4 d) (r4 d t * Real.cos t) t

theorem GerverSofa.PartF.Integrals.Y4_hasDerivAt (d : Reduced.Params) (t : ℝ) : HasDerivAt (Y4 d) (-r4 d t * Real.sin t) t

theorem GerverSofa.PartF.Integrals.X1_join (d : Reduced.Params) : X1 d d.phi = X2 d d.phi

theorem GerverSofa.PartF.Integrals.Y1_join (d : Reduced.Params) : Y1 d d.phi = Y2 d d.phi

theorem GerverSofa.PartF.Integrals.X2_join (d : Reduced.Params) : X2 d d.theta = X3 d d.theta

theorem GerverSofa.PartF.Integrals.Y2_join (d : Reduced.Params) : Y2 d d.theta = Y3 d d.theta

theorem GerverSofa.PartF.Integrals.fourth_equation (d : Reduced.Params) (hd : Reduced.Equations d) : d.a + Phases.T - d.phi - d.theta - d.b + 1 / 2 * (d.theta - d.phi) * (1 + d.a) + 1 / 4 * (d.theta - d.phi) * (d.theta - d.phi) = 0

theorem GerverSofa.PartF.Integrals.X3_join (d : Reduced.Params) (hd : Reduced.Equations d) : X3 d (eta d) = X4 d (eta d)

theorem GerverSofa.PartF.Integrals.Y3_join (d : Reduced.Params) (hd : Reduced.Equations d) : Y3 d (eta d) = Y4 d (eta d)

theorem GerverSofa.PartF.Integrals.X4_terminal (d : Reduced.Params) : X4 d (tau d) = 1

theorem GerverSofa.PartF.Integrals.Y4_terminal (d : Reduced.Params) : Y4 d (tau d) = 0

theorem GerverSofa.PartF.Integrals.r_phase1 (d : Reduced.Params) {t : ℝ} (ht : t ≤ d.phi) : r d t = r1 d t

theorem GerverSofa.PartF.Integrals.r_phase2 (d : Reduced.Params) {t : ℝ} (hlo : d.phi < t) (hhi : t ≤ d.theta) : r d t = r2 d t

theorem GerverSofa.PartF.Integrals.r_phase3 (d : Reduced.Params) (ho : Ordered d) {t : ℝ} (hlo : d.theta < t) (hhi : t ≤ eta d) : r d t = r3 d t

theorem GerverSofa.PartF.Integrals.r_phase4 (d : Reduced.Params) (ho : Ordered d) {t : ℝ} (hlo : eta d < t) (hhi : t ≤ tau d) : r d t = r4 d t

F04: evaluation of the literal integrals on all four closed intervals

The fundamental theorem is applied to smooth branch primitives. Equality with the discontinuous integrand is required only on the open interval. Adjacent integrals are then added, using the proved matching values at every switch.

theorem GerverSofa.PartF.Integrals.integrate_branch (f f' P : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf' : Continuous f') (hderiv : ∀ (t : ℝ), HasDerivAt P (f' t) t) (heq : ∀ t ∈ Set.Ioo a b, f t = f' t) : IntervalIntegrable f MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, f t = P b - P a

theorem GerverSofa.PartF.Integrals.cos_tail4 (d : Reduced.Params) (ho : Ordered d) (t : ℝ) (ht : t ∈ Set.Icc (eta d) (tau d)) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.cos u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.cos u = 1 - X4 d t

theorem GerverSofa.PartF.Integrals.sin_tail4 (d : Reduced.Params) (ho : Ordered d) (t : ℝ) (ht : t ∈ Set.Icc (eta d) (tau d)) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.sin u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.sin u = Y4 d t

theorem GerverSofa.PartF.Integrals.cos_tail3 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.theta (eta d)) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.cos u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.cos u = 1 - X3 d t

theorem GerverSofa.PartF.Integrals.sin_tail3 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.theta (eta d)) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.sin u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.sin u = Y3 d t

theorem GerverSofa.PartF.Integrals.cos_tail2 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.phi d.theta) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.cos u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.cos u = 1 - X2 d t

theorem GerverSofa.PartF.Integrals.sin_tail2 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.phi d.theta) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.sin u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.sin u = Y2 d t

theorem GerverSofa.PartF.Integrals.cos_tail1 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 d.phi) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.cos u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.cos u = 1 - X1 d t

theorem GerverSofa.PartF.Integrals.sin_tail1 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 d.phi) : IntervalIntegrable (fun (u : ℝ) => r d u * Real.sin u) MeasureTheory.volume t (tau d) ∧ ∫ (u : ℝ) in t..tau d, r d u * Real.sin u = Y1 d t

theorem GerverSofa.PartF.Integrals.xi_zeta_phase1 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 d.phi) : xi d t = X1 d t ∧ zeta d t = Y1 d t

theorem GerverSofa.PartF.Integrals.xi_zeta_phase2 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.phi d.theta) : xi d t = X2 d t ∧ zeta d t = Y2 d t

theorem GerverSofa.PartF.Integrals.xi_zeta_phase3 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.theta (eta d)) : xi d t = X3 d t ∧ zeta d t = Y3 d t

theorem GerverSofa.PartF.Integrals.xi_zeta_phase4 (d : Reduced.Params) (ho : Ordered d) (t : ℝ) (ht : t ∈ Set.Icc (eta d) (tau d)) : xi d t = X4 d t ∧ zeta d t = Y4 d t

theorem GerverSofa.PartF.Integrals.xi_zero (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) : xi d 0 = Phases.V1 d

noncomputable def GerverSofa.PartF.Integrals.W (d : Reduced.Params) (t : ℝ) : ℝ

The projection ξ sin t + ζ cos t used in the integral identities.

Equations

• GerverSofa.PartF.Integrals.W d t = GerverSofa.PartF.Integrals.xi d t * Real.sin t + GerverSofa.PartF.Integrals.zeta d t * Real.cos t

theorem GerverSofa.PartF.Integrals.primitive_W (g gp U V t : ℝ) : (V + g * Real.sin t + gp * Real.cos t) * Real.sin t + (U + g * Real.cos t - gp * Real.sin t) * Real.cos t = g + U * Real.cos t + V * Real.sin t

theorem GerverSofa.PartF.Integrals.W_phase1 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 d.phi) : W d t = r1 d t + Phases.U1 d * Real.cos t + Phases.V1 d * Real.sin t

theorem GerverSofa.PartF.Integrals.W_phase2 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.phi d.theta) : W d t = Phases.g2 d t + Phases.U2 d * Real.cos t + Phases.V2 d * Real.sin t

theorem GerverSofa.PartF.Integrals.W_phase3 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc d.theta (eta d)) : W d t = Phases.g3 d t + Phases.U3 d * Real.cos t + Phases.V3 d * Real.sin t

theorem GerverSofa.PartF.Integrals.W_phase4 (d : Reduced.Params) (ho : Ordered d) (t : ℝ) (ht : t ∈ Set.Icc (eta d) (tau d)) : W d t = Phases.g4 d t + Phases.U4 d * Real.cos t + Phases.V4 d * Real.sin t

F05: the four-parameter dictionary satisfies the full 22 equations

These polynomial certificates use the four reduced equations and the two trigonometric circle identities. No box membership or uniqueness is assumed. They do not identify the dictionary with the independently certified 22D root. The module is independent of the F04 integral evaluation.

theorem GerverSofa.PartF.Phases.dictionary_equations (d : Reduced.Params) (hd : Reduced.Equations d) : Romik.Equations (dictionary d)

noncomputable def GerverSofa.PartF.Phases.undictionary (p : Romik.Params) : Reduced.Params

Read back the four free parameters from the 22D representation.

Equations

• GerverSofa.PartF.Phases.undictionary p = { a := p.phi - 1 - 2 * p.b1, b := p.b2 + 1 / 2 - (1 + (p.phi - 1 - 2 * p.b1)) * p.phi / 2 + p.phi ^ 2 / 4, phi := p.phi, theta := p.theta }

theorem GerverSofa.PartF.Phases.undictionary_dictionary (d : Reduced.Params) : undictionary (dictionary d) = d

F06: reverse reduction from the full Romik equations

This direction uses velocity matching and the two contact equations. It does not assume membership in either numerical box or any strict angle inequality.

theorem GerverSofa.PartF.Phases.rot_injective (t : ℝ) : Function.Injective (Romik.rot t)

theorem GerverSofa.PartF.Phases.alphaBeta12_eq {p : Romik.Params} (hp : Romik.Equations p) : Romik.alphaBeta1 p p.phi = Romik.alphaBeta2 p p.phi

theorem GerverSofa.PartF.Phases.alphaBeta23_eq {p : Romik.Params} (hp : Romik.Equations p) : Romik.alphaBeta2 p p.theta = Romik.alphaBeta3 p p.theta

theorem GerverSofa.PartF.Phases.c2_eq_of_full {p : Romik.Params} (hp : Romik.Equations p) : p.c2 = -2 - 2 * p.b1

theorem GerverSofa.PartF.Phases.c1_eq_of_full {p : Romik.Params} (hp : Romik.Equations p) : p.c1 = Real.pi / 2 - 2 - 2 * p.b1

theorem GerverSofa.PartF.Phases.reverse_equation4 {p : Romik.Params} (hp : Romik.Equations p) : Reduced.system (undictionary p) 3 = 0

theorem GerverSofa.PartF.Phases.reverse_equation3 {p : Romik.Params} (hp : Romik.Equations p) : Reduced.system (undictionary p) 2 = 0

theorem GerverSofa.PartF.Phases.reverse_equation1 {p : Romik.Params} (hp : Romik.Equations p) : Reduced.system (undictionary p) 0 = 0

theorem GerverSofa.PartF.Phases.reverse_equation2 {p : Romik.Params} (hp : Romik.Equations p) : Reduced.system (undictionary p) 1 = 0

theorem GerverSofa.PartF.Phases.undictionary_equations {p : Romik.Params} (hp : Romik.Equations p) : Reduced.Equations (undictionary p)

F06: the reverse parameters determine the full solution

Velocity matching determines the shape coefficients. Positional matching then determines each successive translation. No numerical enclosure is used.

theorem GerverSofa.PartF.Phases.full_equations_injective {p q : Romik.Params} (hp : Romik.Equations p) (hq : Romik.Equations q) (h : undictionary p = undictionary q) : p = q

theorem GerverSofa.PartF.Phases.dictionary_undictionary_of_equations {p : Romik.Params} (hp : Romik.Equations p) : dictionary (undictionary p) = p