Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartF.Semantics.Batch002.

Gerver sofa dependency batch

• KernelOnly.PartF.F01ExistingMotion.
• KernelOnly.PartF.F01ParameterChoice.
• KernelOnly.PartF.F02EuclideanMotion.
• KernelOnly.PartF.F03CanonicalRotation.
• KernelOnly.PartF.F03SetIdentification.
• KernelOnly.PartF.F04IntegralRepresentation.
• KernelOnly.PartF.F06ParameterIdentification.
• KernelOnly.PartF.F06IntegralMotion.

F01: exact identity normalization of the already certified motion

The original project asks for an initial translation. For its concrete Gerver path the inverse frame is exactly the identity, which is the stronger normalization required by DeepMind. These statements refer to the existing ℝ × ℝ coordinate model, not to an unproved isometry between the product norm and the Euclidean norm.

noncomputable def GerverSofa.PartF.Existing.motion (s : ℝ) : SE2

Invert the hallway frame to obtain the sofa’s rigid motion.

Equations

• GerverSofa.PartF.Existing.motion s = (GerverSofa.PartC.frame s).inv

theorem GerverSofa.PartF.Existing.motion_zero : motion 0 = SE2.one

theorem GerverSofa.PartF.Existing.motion_continuous : SE2.ContinuousPath motion

theorem GerverSofa.PartF.Existing.initial : PartC.G ⊆ horizontalArm

theorem GerverSofa.PartF.Existing.all_times (s : ℝ) : s ∈ Set.Icc 0 1 → (motion s).act '' PartC.G ⊆ hallway

theorem GerverSofa.PartF.Existing.final : (motion 1).act '' PartC.G ⊆ verticalArm

F01: parameter selection is independent of the existence proof

This module reuses the frozen E24KC6 theorem. It does not repeat numerical exclusion. The literal upstream order of conjunctions is checked against the existing specification, and its selected tuple is identified with the certified reduced solution. No identification with the full 22D tuple is claimed by this module.

def GerverSofa.PartF.Parameters.upstreamSpec (A B φ θ : ℝ) : Prop

The nonnegative parameter and ordered-angle equations used by the upstream canonical definition.

Equations

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

theorem GerverSofa.PartF.Parameters.upstreamSpec_iff (A B φ θ : ℝ) : upstreamSpec A B φ θ ↔ PartE.DeepMindABPhiThetaSpec A B φ θ

def GerverSofa.PartF.Parameters.TupleSpec (q : ℝ × ℝ × ℝ × ℝ) : Prop

Package the upstream four-parameter specification as a predicate on a nested tuple.

Equations

• GerverSofa.PartF.Parameters.TupleSpec q = GerverSofa.PartF.Parameters.upstreamSpec q.1 q.2.1 q.2.2.1 q.2.2.2

theorem GerverSofa.PartF.Parameters.existsUnique : ∃! q : ℝ × ℝ × ℝ × ℝ, TupleSpec q

noncomputable def GerverSofa.PartF.Parameters.certified : ℝ × ℝ × ℝ × ℝ

The certified reduced solution converted to the upstream four-parameter tuple.

Equations

• GerverSofa.PartF.Parameters.certified = GerverSofa.PartE.tupleEquiv.symm GerverSofa.PartALeanCert.reducedCertifiedUniqueSolution.solution

theorem GerverSofa.PartF.Parameters.certified_spec : TupleSpec certified

theorem GerverSofa.PartF.Parameters.any_solution_eq_certified (q : ℝ × ℝ × ℝ × ℝ) (hq : TupleSpec q) : q = certified

theorem GerverSofa.PartF.Parameters.choice_independent (h : ∃! q : ℝ × ℝ × ℝ × ℝ, TupleSpec q) : Exists.choose h = certified

This applies to any eventual upstream proof of the same specification.

F02: the certified sofa as a set with Euclidean rigid motion

Every existing SE2 action is realized by an affine isometry of Plane. Norm preservation is proved in Plane from the equation c*c+s*s=1. Continuity is proved in the induced continuous-affine-map topology of F01. The final theorem transfers all seven motion fields for the already certified set, without adding geometric hypotheses.

This module does not identify the set with the literal upstream integral definition. Its rotation matrices are explicit; their comparison with F01.rotation and the integral representation are separate bridge steps.

def GerverSofa.PartF.EuclideanMotion.linearPart (g : SE2) : Plane ≃ₗ[ℝ] Plane

The standard rotation matrix associated with an existing SE2 value.

Equations

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

@[simp]

theorem GerverSofa.PartF.EuclideanMotion.linearPart_zero_coord (g : SE2) (q : Plane) : ((linearPart g) q).ofLp 0 = g.c * q.ofLp 0 - g.s * q.ofLp 1

@[simp]

theorem GerverSofa.PartF.EuclideanMotion.linearPart_one_coord (g : SE2) (q : Plane) : ((linearPart g) q).ofLp 1 = g.s * q.ofLp 0 + g.c * q.ofLp 1

theorem GerverSofa.PartF.EuclideanMotion.linearPart_norm_sq (g : SE2) (q : Plane) : ‖(linearPart g) q‖ ^ 2 = ‖q‖ ^ 2

theorem GerverSofa.PartF.EuclideanMotion.linearPart_norm (g : SE2) (q : Plane) : ‖(linearPart g) q‖ = ‖q‖

def GerverSofa.PartF.EuclideanMotion.linearIsometry (g : SE2) : Plane ≃ₗᵢ[ℝ] Plane

The linear isometry determined by the rotation coefficients of an SE2 motion.

Equations

• GerverSofa.PartF.EuclideanMotion.linearIsometry g = { toLinearEquiv := GerverSofa.PartF.EuclideanMotion.linearPart g, norm_map' := ⋯ }

noncomputable def GerverSofa.PartF.EuclideanMotion.ofSE2 (g : SE2) : Rigid

A genuine Euclidean affine isometry with the original coordinate action.

Equations

• GerverSofa.PartF.EuclideanMotion.ofSE2 g = GerverSofa.PartF.rotateThenTranslate (GerverSofa.PartF.EuclideanMotion.linearIsometry g) (GerverSofa.PartF.Coordinates.toPlane (g.tx, g.ty))

theorem GerverSofa.PartF.EuclideanMotion.ofSE2_apply (g : SE2) (q : Plane) : (ofSE2 g) q = Coordinates.toPlane (g.act (Coordinates.fromPlane q))

theorem GerverSofa.PartF.EuclideanMotion.ofSE2_apply_toPlane (g : SE2) (q : Point) : (ofSE2 g) (Coordinates.toPlane q) = Coordinates.toPlane (g.act q)

theorem GerverSofa.PartF.EuclideanMotion.ofSE2_one : ofSE2 SE2.one = AffineIsometryEquiv.refl ℝ Plane

theorem GerverSofa.PartF.EuclideanMotion.image_action (g : SE2) (S : Set Point) : ⇑(ofSE2 g) '' Coordinates.toPlane '' S = Coordinates.toPlane '' g.act '' S

def GerverSofa.PartF.EuclideanMotion.quarterTurnLinear : Plane →ₗ[ℝ] Plane

The coordinate quarter-turn, used to express continuous matrix coefficients.

Equations

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

noncomputable def GerverSofa.PartF.EuclideanMotion.quarterTurn : Plane →L[ℝ] Plane

The quarter-turn rotation bundled as a continuous linear map.

Equations

• GerverSofa.PartF.EuclideanMotion.quarterTurn = LinearMap.toContinuousLinearMap GerverSofa.PartF.EuclideanMotion.quarterTurnLinear

theorem GerverSofa.PartF.EuclideanMotion.continuous_ofSE2 {X : Type u_1} [TopologicalSpace X] (g : X → SE2) (hc : Continuous fun (t : X) => (g t).c) (hs : Continuous fun (t : X) => (g t).s) (htx : Continuous fun (t : X) => (g t).tx) (hty : Continuous fun (t : X) => (g t).ty) : Continuous fun (t : X) => ofSE2 (g t)

Componentwise continuous SE2 coefficients give continuity in the actual topology on affine isometry equivalences.

theorem GerverSofa.PartF.EuclideanMotion.continuous_ofSE2_path (g : ℝ → SE2) (hg : SE2.ContinuousPath g) : Continuous fun (t : ℝ) => ofSE2 (g t)

def GerverSofa.PartF.EuclideanMotion.sofa : Set Plane

The coordinate image of the certified Gerver sofa in the Euclidean plane.

Equations

• GerverSofa.PartF.EuclideanMotion.sofa = GerverSofa.PartF.Coordinates.toPlane '' GerverSofa.PartC.G

noncomputable def GerverSofa.PartF.EuclideanMotion.motion (s : ↑unitInterval) : Rigid

The certified sofa motion as affine isometries indexed by the unit interval.

Equations

• GerverSofa.PartF.EuclideanMotion.motion s = GerverSofa.PartF.EuclideanMotion.ofSE2 (GerverSofa.PartF.Existing.motion ↑s)

theorem GerverSofa.PartF.EuclideanMotion.motion_continuous : Continuous motion

theorem GerverSofa.PartF.EuclideanMotion.concrete_movingSofa : Model.IsMovingSofa sofa motion

All seven motion requirements hold for the coordinate image of the already certified Gerver set. No additional geometric assumptions occur.

F03: the upstream-oriented rotation in the certified coordinates

The orientation is the ordered coordinate-basis orientation installed in F01, with the same definition as the pinned upstream plane helper. We compute its area form, then its right-angle rotation, before comparing rotation matrices. No replacement orientation or additional orientation hypothesis is introduced.

theorem GerverSofa.PartF.CanonicalRotation.areaForm_coordinates (q r : Plane) : (EuclideanGeometry.o.areaForm q) r = q.ofLp 0 * r.ofLp 1 - q.ofLp 1 * r.ofLp 0

The sign is fixed by the ordered orthonormal coordinate basis.

theorem GerverSofa.PartF.CanonicalRotation.rightAngleRotation_apply (q : Plane) : EuclideanGeometry.o.rightAngleRotation q = Coordinates.toPlane (-q.ofLp 1, q.ofLp 0)

The positive quarter-turn is exactly (x,y) ↦ (-y,x).

theorem GerverSofa.PartF.CanonicalRotation.rotation_apply (t : ℝ) (q : Plane) : (rotation t) q = Coordinates.toPlane (Romik.rot t (Coordinates.fromPlane q))

theorem GerverSofa.PartF.CanonicalRotation.rotation_toPlane (t : ℝ) (q : Point) : (rotation t) (Coordinates.toPlane q) = Coordinates.toPlane (Romik.rot t q)

theorem GerverSofa.PartF.CanonicalRotation.linearIsometry_eq_rotation (g : SE2) (t : ℝ) (hc : g.c = Real.cos t) (hs : g.s = Real.sin t) : EuclideanMotion.linearIsometry g = rotation t

theorem GerverSofa.PartF.CanonicalRotation.ofSE2_eq_worldFrame (g : SE2) (t : ℝ) (hc : g.c = Real.cos t) (hs : g.s = Real.sin t) : EuclideanMotion.ofSE2 g = worldFrame t (Coordinates.toPlane (g.tx, g.ty))

theorem GerverSofa.PartF.CanonicalRotation.romikFrame_eq_worldFrame (p : Romik.Params) (s : ℝ) : EuclideanMotion.ofSE2 (Romik.frame p s) = worldFrame (Romik.angle s) (Coordinates.toPlane (Romik.path p (Romik.angle s)))

The physical angle is s * (π/2), including both endpoints.

theorem GerverSofa.PartF.CanonicalRotation.romikFrame_zero_act (p : Romik.Params) (hzero : Romik.path p 0 = (0, 0)) (q : Point) : (Romik.frame p 0).act q = q

theorem GerverSofa.PartF.CanonicalRotation.closedPath_rotation (d : Reduced.Params) (hd : Reduced.Equations d) (t : ℝ) : (rotation t) (Coordinates.toPlane (Phases.closedPath d t)) = Coordinates.toPlane (Romik.path (Phases.dictionary d) t)

The already proved five-phase algebra now uses the canonical rotation.

F03: the certified set as a canonical hallway intersection

We transport the existing reconstruction theorem, including the endpoint arms, to the Euclidean world-frame convention. The final conditional interfaces state the outstanding path/dictionary equalities explicitly. They do not prove the literal integral representation or identify the certified 22D tuple.

theorem GerverSofa.PartF.SetIdentification.mem_coordinate_image (S : Set Point) (q : Plane) : q ∈ Coordinates.toPlane '' S ↔ Coordinates.fromPlane q ∈ S

theorem GerverSofa.PartF.SetIdentification.mem_ofSE2_image (g : SE2) (S : Set Point) (q : Plane) : q ∈ ⇑(EuclideanMotion.ofSE2 g) '' Coordinates.toPlane '' S ↔ Coordinates.fromPlane q ∈ g.act '' S

theorem GerverSofa.PartF.SetIdentification.reconstructedSet_image (p : Romik.Params) (hzero : Romik.path p 0 = (0, 0)) : Coordinates.toPlane '' Romik.reconstructedSet p = frameIntersection (fun (s : ↑unitInterval) => EuclideanMotion.ofSE2 (Romik.frame p ↑s)) Model.horizontalHallway Model.verticalHallway Model.hallway

The change from real unit time to subtype unit time loses no constraint.

theorem GerverSofa.PartF.SetIdentification.reconstructedSet_image_eq_worldSofa (p : Romik.Params) (hzero : Romik.path p 0 = (0, 0)) : Coordinates.toPlane '' Romik.reconstructedSet p = worldSofa (fun (t : ℝ) => Coordinates.toPlane (Romik.path p t)) Model.horizontalHallway Model.verticalHallway Model.hallway

theorem GerverSofa.PartF.SetIdentification.sofa_eq_worldSofa : EuclideanMotion.sofa = worldSofa (fun (t : ℝ) => Coordinates.toPlane (Romik.path PartC.params t)) Model.horizontalHallway Model.verticalHallway Model.hallway

An unconditional identification of the concrete, already certified set.

F04: the literal integral path equals the closed five-phase path

All integral identities are proved in F04IntegralEvaluation. Reflection of the closed intervals then gives the same five branches and the same endpoint choices as F01. The final identification with PartC.params still requires the 22D dictionary theorem; it remains an explicit hypothesis in the two last results.

theorem GerverSofa.PartF.Integrals.path_first_of_le (d : Reduced.Params) (t : ℝ) (ht : t ≤ d.phi) : (path d t).1 = Real.cos t - 1

theorem GerverSofa.PartF.Integrals.path_first_of_gt (d : Reduced.Params) (t : ℝ) (ht : d.phi < t) : (path d t).1 = W d (Phases.T - t) - 1

theorem GerverSofa.PartF.Integrals.path_second_of_le (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ≤ tau d) : (path d t).2 = W d t - Phases.ell d * Real.sin t - 1

theorem GerverSofa.PartF.Integrals.path_second_of_gt (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : tau d < t) : (path d t).2 = (1 - Phases.ell d) * Real.sin t - 1

theorem GerverSofa.PartF.Integrals.path_phase1 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 d.phi) : path d t = Phases.closed1 d t

theorem GerverSofa.PartF.Integrals.path_phase2 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (hlo : d.phi < t) (hhi : t ≤ d.theta) : path d t = Phases.closed2 d t

theorem GerverSofa.PartF.Integrals.path_phase3 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (hlo : d.theta < t) (hhi : t ≤ eta d) : path d t = Phases.closed3 d t

theorem GerverSofa.PartF.Integrals.path_phase4 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (hlo : eta d < t) (hhi : t ≤ tau d) : path d t = Phases.closed4 d t

theorem GerverSofa.PartF.Integrals.path_phase5 (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (hlo : tau d < t) (hhi : t ≤ Phases.T) : path d t = Phases.closed5 d t

theorem GerverSofa.PartF.Integrals.path_eq_closedPath (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 Phases.T) : path d t = Phases.closedPath d t

The literal integral path, not just its formal candidate, has these phases.

theorem GerverSofa.PartF.Integrals.integral_rotation (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) (t : ℝ) (ht : t ∈ Set.Icc 0 Phases.T) : (rotation t) (Coordinates.toPlane (path d t)) = Coordinates.toPlane (Romik.path (Phases.dictionary d) t)

theorem GerverSofa.PartF.Integrals.integral_sofa_eq_worldSofa (d : Reduced.Params) (ho : Ordered d) (hd : Reduced.Equations d) : bodySofa (fun (t : ℝ) => Coordinates.toPlane (path d t)) Model.horizontalHallway Model.verticalHallway Model.hallway = worldSofa (fun (t : ℝ) => Coordinates.toPlane (Romik.path (Phases.dictionary d) t)) Model.horizontalHallway Model.verticalHallway Model.hallway

noncomputable def GerverSofa.PartF.Integrals.certified : Reduced.Params

The reduced parameters selected by the concrete uniqueness certificate.

Equations

• GerverSofa.PartF.Integrals.certified = GerverSofa.PartALeanCert.reducedCertifiedUniqueSolution.solution

theorem GerverSofa.PartF.Integrals.certified_ordered : Ordered certified

theorem GerverSofa.PartF.Integrals.certified_equations : Reduced.Equations certified

theorem GerverSofa.PartF.Integrals.certified_integral_rotation (t : ℝ) (ht : t ∈ Set.Icc 0 Phases.T) : (rotation t) (Coordinates.toPlane (path certified t)) = Coordinates.toPlane (Romik.path (Phases.dictionary certified) t)

An unconditional representation theorem for the certified reduced tuple.

theorem GerverSofa.PartF.Integrals.integral_sofa_eq_certified_of_dictionary (hdictionary : Phases.dictionary certified = PartC.params) : bodySofa (fun (t : ℝ) => Coordinates.toPlane (path certified t)) Model.horizontalHallway Model.verticalHallway Model.hallway = EuclideanMotion.sofa

Remaining obligation: identify the full dictionary with the independent 22D root.

F06: identify the two independently certified parameter choices

The 22D box supplies only coarse physical inequalities for its reverse parameters. Global 4D uniqueness from Part E then identifies the reduced root. The full algebraic reconstruction closes the 22D identity without a new Krawczyk run or a forward enclosure into the narrow full box.

theorem GerverSofa.PartF.Parameters.undictionary_physical_of_mem_full_box {p : Romik.Params} (hp : p ∈ Romik.box) : PartE.PhysicalDomain (Phases.undictionary p)

theorem GerverSofa.PartF.Parameters.undictionary_eq_reduced_certified {p : Romik.Params} (hp : p ∈ Romik.box) (heq : Romik.Equations p) : Phases.undictionary p = PartALeanCert.reducedCertifiedUniqueSolution.solution

theorem GerverSofa.PartF.Parameters.dictionary_eq_full_certified : Phases.dictionary PartALeanCert.reducedCertifiedUniqueSolution.solution = PartB.params

F06: unconditional motion bridge for the literal integral construction

This is the translate-then-rotate body model defined in Part F, with the canonical Euclidean orientation. It does not silently replace the current upstream rotateTranslate definition discussed in issue #5270.

theorem GerverSofa.PartF.Integrals.certified_dictionary_eq_params : Phases.dictionary certified = PartC.params

theorem GerverSofa.PartF.Integrals.certified_integral_rotation_to_full (t : ℝ) (ht : t ∈ Set.Icc 0 Phases.T) : (rotation t) (Coordinates.toPlane (path certified t)) = Coordinates.toPlane (Romik.path PartC.params t)

theorem GerverSofa.PartF.Integrals.integral_sofa_eq_certified : bodySofa (fun (t : ℝ) => Coordinates.toPlane (path certified t)) Model.horizontalHallway Model.verticalHallway Model.hallway = EuclideanMotion.sofa