Gerver sofa: related certificate and semantic modules

• GerverSofa.KernelOnly.PartC.Semantics.Batch001.

Gerver sofa dependency batch

• KernelOnly.PartC.Definitions.
• KernelOnly.PartC.Parameters.
• KernelOnly.PartC.ContactAlgebra.
• KernelOnly.PartC.GlobalSupport.
• KernelOnly.PartC.BaseGeometry.
• KernelOnly.PartC.TopologySpec.
• KernelOnly.PartC.GeometrySpec.
• KernelOnly.PartC.Stage2.MeshFacts.
• KernelOnly.PartC.Stage2.EnvelopeAlgebra.
• KernelOnly.PartC.Stage2.NoHiddenCore.
• KernelOnly.PartC.Stage2.SupportPhaseDerivatives.
• KernelOnly.PartC.Stage3.SupportDirect.
• KernelOnly.PartC.Stage3.FinalClosureDirect.
• KernelOnly.PartC.Stage4.PathDifferential.
• KernelOnly.PartC.Stage4.ExactGeometryFacts.
• KernelOnly.PartC.Stage4.NoHiddenMatchFacts.
• KernelOnly.PartC.Stage4.NoHiddenContinuityFacts.
• KernelOnly.PartC.Stage4.NoHiddenSignFacts.
• KernelOnly.PartC.Stage4.NoHiddenTurningFacts.
• KernelOnly.PartC.Stage4.NoHiddenDifferentialFacts.
• KernelOnly.PartC.Stage4.NoHiddenReflectionFacts.
• KernelOnly.PartC.Stage4.NoHiddenDirect.
• KernelOnly.PartC.Stage4.NicheEnvelopeSupport.
• KernelOnly.PartC.Stage4.SofaConvexityFacts.
• KernelOnly.PartC.Stage4.VerticalFillTopology.
• KernelOnly.PartC.Stage4.WallGraphs.
• KernelOnly.PartC.Stage4.NicheMembershipFacts.
• KernelOnly.PartC.Stage4.NicheFrontierTopology.
• KernelOnly.PartC.Stage4.NicheConnectedDirect.
• KernelOnly.PartC.Stage4.SofaFiberTopology.
• KernelOnly.PartC.Stage4.SofaTopologyDirect.
• KernelOnly.PartC.Stage4.FinalTopologyClosure.

Part C concrete objects

This file fixes the exact objects used throughout Part C. The numerical root, regularity and global two-variable support margins are inherited from the closed Parts A and B. No alternative parameter vector or geometric set is introduced here.

@[reducible, inline]

noncomputable abbrev GerverSofa.PartC.params : Romik.Params

The certified twenty-two dimensional Gerver parameter vector.

Equations

• GerverSofa.PartC.params = GerverSofa.PartB.params

noncomputable def GerverSofa.PartC.T : ℝ

Physical terminal angle.

Equations

• GerverSofa.PartC.T = Real.pi / 2

noncomputable def GerverSofa.PartC.eta : ℝ

Reflected switching angles.

Equations

• GerverSofa.PartC.eta = GerverSofa.PartC.T - GerverSofa.PartC.params.theta

noncomputable def GerverSofa.PartC.tau : ℝ

The reflected switching angle π/2 - φ for the certified parameters.

Equations

• GerverSofa.PartC.tau = GerverSofa.PartC.T - GerverSofa.PartC.params.phi

@[reducible, inline]

abbrev GerverSofa.PartC.K : Set Point

The concrete cap, fixed sofa, reconstructed Romik set and frame.

Equations

• GerverSofa.PartC.K = GerverSofa.Romik.K0 GerverSofa.PartC.params

@[reducible, inline]

abbrev GerverSofa.PartC.G : Set Point

The fixed Gerver sofa at the certified Romik parameters.

Equations

• GerverSofa.PartC.G = GerverSofa.Romik.sofa GerverSofa.PartC.params

@[reducible, inline]

abbrev GerverSofa.PartC.Sx : Set Point

The reconstructed contact-curve set at the certified parameters.

Equations

• GerverSofa.PartC.Sx = GerverSofa.Romik.reconstructedSet GerverSofa.PartC.params

@[reducible, inline]

noncomputable abbrev GerverSofa.PartC.frame : ℝ → SE2

The rigid frame path determined by the certified Romik parameters.

Equations

• GerverSofa.PartC.frame = GerverSofa.Romik.frame GerverSofa.PartC.params

def GerverSofa.PartC.anchor : Point

Endpoint support point used for the direct nonemptiness proof.

Equations

• GerverSofa.PartC.anchor = (1, 0)

noncomputable def GerverSofa.PartC.alphaBetaAt (t : ℝ) : Point

Piecewise body-frame derivative coefficients. This definition is local to Part C so that the geometric layer does not import the later Part D article claims.

Equations

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

noncomputable def GerverSofa.PartC.alpha (t : ℝ) : ℝ

The horizontal body-frame velocity coefficient.

Equations

• GerverSofa.PartC.alpha t = (GerverSofa.PartC.alphaBetaAt t).1

noncomputable def GerverSofa.PartC.beta (t : ℝ) : ℝ

The vertical body-frame velocity coefficient.

Equations

• GerverSofa.PartC.beta t = (GerverSofa.PartC.alphaBetaAt t).2

noncomputable def GerverSofa.PartC.A (t : ℝ) : Point

The four standard contact curves.

Equations

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

noncomputable def GerverSofa.PartC.B (t : ℝ) : Point

The inner contact curve x + α v.

Equations

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

noncomputable def GerverSofa.PartC.C (t : ℝ) : Point

The outer contact curve x - β u + v.

Equations

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

noncomputable def GerverSofa.PartC.D (t : ℝ) : Point

The inner contact curve x - β u.

Equations

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

def GerverSofa.PartC.curveImage (f : ℝ → Point) (I : Set ℝ) : Set Point

Image of a parametrized curve over a time set.

Equations

• GerverSofa.PartC.curveImage f I = f '' I

def GerverSofa.PartC.lineSegment (a b : Point) : Set Point

A closed line segment, written without depending on a specialized convex geometry API.

Equations

• GerverSofa.PartC.lineSegment a b = {q : GerverSofa.Point | ∃ r ∈ Set.Icc 0 1, q = ((1 - r) * a.1 + r * b.1, (1 - r) * a.2 + r * b.2)}

def GerverSofa.PartC.claimedNicheBoundary : Set Point

Set-valued form of the niche boundary described in the manuscript.

Equations

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

Frozen parameter and endpoint consequences for Part C

theorem GerverSofa.PartC.params_mem : params ∈ Romik.box

theorem GerverSofa.PartC.params_equations : Romik.Equations params

theorem GerverSofa.PartC.switchOrder : Romik.SwitchOrder params

theorem GerverSofa.PartC.pathContinuous : Continuous (Romik.path params)

theorem GerverSofa.PartC.frameContinuous : SE2.ContinuousPath frame

theorem GerverSofa.PartC.pathZero : Romik.path params 0 = (0, 0)

theorem GerverSofa.PartC.pathEndYZero : (Romik.path params T).2 = 0

theorem GerverSofa.PartC.phi_bounds : 1958868239504182093160893749 / 50000000000000000000000000000 ≤ params.phi ∧ params.phi ≤ 78354729580167283726435751 / 2000000000000000000000000000

theorem GerverSofa.PartC.theta_bounds : 34065075469136244723692787727 / 50000000000000000000000000000 ≤ params.theta ∧ params.theta ≤ 34065075469136244723692787983 / 50000000000000000000000000000

Exact contact-curve algebra

These identities are independent of every interval estimate. They record that A and C lie on the two outer supporting lines, while B and D lie on the corresponding inner-wall lines. Later geometric work only has to prove that the relevant contact points belong to the cap and that no hidden crossing changes the boundary envelope.

theorem GerverSofa.PartC.A_support_identity (t : ℝ) : dot (A t) (u t) = dot (Romik.path params t) (u t) + 1

A(t) lies on the first outer support line.

theorem GerverSofa.PartC.C_support_identity (t : ℝ) : dot (C t) (v t) = dot (Romik.path params t) (v t) + 1

C(t) lies on the second outer support line.

theorem GerverSofa.PartC.B_inner_u_identity (t : ℝ) : dot (B t - Romik.path params t) (u t) = 0

B(t) lies on the first inner wall through the corner path.

theorem GerverSofa.PartC.D_inner_v_identity (t : ℝ) : dot (D t - Romik.path params t) (v t) = 0

D(t) lies on the second inner wall through the corner path.

Consequences of the certified Part B continuum margins

The two strict inequalities already certified on the complete square imply that every point of the Gerver rotation path satisfies every outer supporting half-plane inequality. This is one of the main bridges from Part B into the global geometry of Part C.

theorem GerverSofa.PartC.Gu_positive {s t : ℝ} (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) : 0 < PartB.Gu s t

theorem GerverSofa.PartC.Gv_positive {s t : ℝ} (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) : 0 < PartB.Gv s t

theorem GerverSofa.PartC.path_mem_supportHalfU {s t : ℝ} (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) : Romik.path params t ∈ supportHalfU params s

Every path point lies in every first outer supporting half-plane.

theorem GerverSofa.PartC.path_mem_supportHalfV {s t : ℝ} (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) : Romik.path params t ∈ supportHalfV params s

Every path point lies in every second outer supporting half-plane.

theorem GerverSofa.PartC.path_mem_outer_supports {s t : ℝ} (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) : Romik.path params t ∈ supportHalfU params s ∩ supportHalfV params s

Part C geometric consequences already closed by the existing source

Closedness, supporting-hallway containment, endpoint arms, motion continuity and the set-theoretic identification with Romik's reconstruction require no new numerical replay. They are collected here for the concrete certified parameter vector.

theorem GerverSofa.PartC.closed_G : IsClosed G

theorem GerverSofa.PartC.G_subset_hallway (s : ℝ) : s ∈ Set.Icc 0 1 → G ⊆ Romik.hallwayAt params s

theorem GerverSofa.PartC.initialArm : (frame 0).inv.act '' G ⊆ horizontalArm

theorem GerverSofa.PartC.finalArm : (frame 1).inv.act '' G ⊆ verticalArm

theorem GerverSofa.PartC.G_eq_Sx : G = Sx

Exact topology target for the concrete Gerver set

This file states, but does not postulate, the two genuinely remaining set-theoretic obligations. A later concrete proof must construct a value of TopologyCertificate; until then Part C cannot close.

structure GerverSofa.PartC.TopologyCertificate : Prop

Direct topology certificate with the manuscript's explicit endpoint support witness, rather than an anonymous existential.

• anchor_mem : anchor ∈ G
• connected : IsConnected G

theorem GerverSofa.PartC.TopologyCertificate.nonempty (cert : TopologyCertificate) : G.Nonempty

Global support and niche-topology certificate interfaces

The statements here encode the exact Part C geometry that is not allowed to be hidden inside an arbitrary connected field: contact support, the two no-hidden-crossing inequalities, and the claimed boundary of the niche.

def GerverSofa.PartC.NoHiddenCrossingU : Prop

First no-hidden-crossing inequality from the manuscript.

Equations

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

def GerverSofa.PartC.NoHiddenCrossingV : Prop

Reflected no-hidden-crossing inequality.

Equations

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

structure GerverSofa.PartC.NicheTopologyCertificate : Prop

Proof-carrying niche topology. The boundary equality is set-valued; the orientation and eighteen-piece count belong to the later Part D boundary certificate.

• noHiddenU : NoHiddenCrossingU
• noHiddenV : NoHiddenCrossingV
• boundary_eq : frontier (Romik.niche params) = claimedNicheBoundary
• niche_connected : IsConnected (Romik.niche params)

structure GerverSofa.PartC.GlobalGeometryCertificate : Prop

Complete genuinely new geometry required in Part C.

• supportA (t : ℝ) : t ∈ Set.Icc 0 T → A t ∈ K
• supportC (t : ℝ) : t ∈ Set.Icc 0 T → C t ∈ K
• nicheTopology : NicheTopologyCertificate
• topology : TopologyCertificate

theorem GerverSofa.PartC.GlobalGeometryCertificate.nonempty (cert : GlobalGeometryCertificate) : G.Nonempty

theorem GerverSofa.PartC.GlobalGeometryCertificate.connected (cert : GlobalGeometryCertificate) : IsConnected G

Part C Stage 2 public mesh and branch facts

This module exposes the switch-cell classification already used internally in Part B. It is deliberately proved again from the frozen angle boxes so that Part C contact and no-hidden-crossing certificates can reuse the exact 64-cell mesh without depending on private declarations.

theorem GerverSofa.PartC.Stage2.node1_lt_phi : PartB.nodeTime 1 < params.phi

theorem GerverSofa.PartC.Stage2.phi_lt_node2 : params.phi < PartB.nodeTime 2

theorem GerverSofa.PartC.Stage2.node27_lt_theta : PartB.nodeTime 27 < params.theta

theorem GerverSofa.PartC.Stage2.theta_lt_node28 : params.theta < PartB.nodeTime 28

theorem GerverSofa.PartC.Stage2.node36_lt_eta : PartB.nodeTime 36 < eta

theorem GerverSofa.PartC.Stage2.eta_lt_node37 : eta < PartB.nodeTime 37

theorem GerverSofa.PartC.Stage2.node62_lt_tau : PartB.nodeTime 62 < tau

theorem GerverSofa.PartC.Stage2.tau_lt_node63 : tau < PartB.nodeTime 63

theorem GerverSofa.PartC.Stage2.phase1_cell {i : PartB.Cell} {t : ℝ} (ht : t ∈ PartB.cellSet i) (hphase : t ≤ params.phi) : ↑i ≤ 1

theorem GerverSofa.PartC.Stage2.phase2_cell {i : PartB.Cell} {t : ℝ} (ht : t ∈ PartB.cellSet i) (hlo : params.phi < t) (hhi : t ≤ params.theta) : 1 ≤ ↑i ∧ ↑i ≤ 27

theorem GerverSofa.PartC.Stage2.phase3_cell {i : PartB.Cell} {t : ℝ} (ht : t ∈ PartB.cellSet i) (hlo : params.theta < t) (hhi : t ≤ eta) : 27 ≤ ↑i ∧ ↑i ≤ 36

theorem GerverSofa.PartC.Stage2.phase4_cell {i : PartB.Cell} {t : ℝ} (ht : t ∈ PartB.cellSet i) (hlo : eta < t) (hhi : t ≤ tau) : 36 ≤ ↑i ∧ ↑i ≤ 62

theorem GerverSofa.PartC.Stage2.phase5_cell {i : PartB.Cell} {t : ℝ} (ht : t ∈ PartB.cellSet i) (hlo : tau < t) : 62 ≤ ↑i

theorem GerverSofa.PartC.Stage2.phi_nonneg : 0 ≤ params.phi

theorem GerverSofa.PartC.Stage2.tau_le_T : tau ≤ T

theorem GerverSofa.PartC.Stage2.zero_le_theta : 0 ≤ params.theta

theorem GerverSofa.PartC.Stage2.eta_le_tau : eta ≤ tau

theorem GerverSofa.PartC.Stage2.theta_le_eta : params.theta ≤ eta

Part C Stage 2 redesign: exact envelope algebra

The first 64x64 contact-box attempt was intentionally fail-closed but too coarse at contact/equality cells: interval dependency destroys exact cancellation. This module switches to the analytic envelope coefficients.

For the outer u-contact curve A, the phasewise velocity is a nonnegative scalar multiple of v; for the outer v-contact curve C, the velocity is a nonpositive scalar multiple of u. The scalar coefficients below are the five exact algebraic pieces. No numerical root is recomputed here.

noncomputable def GerverSofa.PartC.Stage2.rhoA (t : ℝ) : ℝ

Phasewise scalar multiplying v(t) in the derivative of A.

Equations

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

noncomputable def GerverSofa.PartC.Stage2.rhoC (t : ℝ) : ℝ

Phasewise nonnegative scalar for C'(t) = -rhoC(t) * u(t).

Equations

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

theorem GerverSofa.PartC.Stage2.rhoA_nonneg {t : ℝ} (ht : t ∈ Set.Icc 0 T) : 0 ≤ rhoA t

The A envelope coefficient is nonnegative on the full physical range.

theorem GerverSofa.PartC.Stage2.rhoC_nonneg {t : ℝ} (ht : t ∈ Set.Icc 0 T) : 0 ≤ rhoC t

The reflected C envelope coefficient is nonnegative on the full physical range.

theorem GerverSofa.PartC.Stage2.A_zero_eq_anchor : A 0 = anchor

The first outer contact starts at the exact fan endpoint (1,0).

theorem GerverSofa.PartC.Stage2.C_T_snd_zero : (C T).2 = 0

The second outer contact ends exactly on the fan boundary.

Exact cell reduction of the two no-hidden-crossing inequalities

Off-diagonal mesh cells are reduced to executable upper bounds for the already sound Part B intervals Gu and Gv. The only analytic remainder after all 128 row certificates pass is the ordered triangle inside each single mesh cell, named SameCellU and SameCellV below.

noncomputable def GerverSofa.PartC.Stage2.UValue (r t : ℝ) : ℝ

Manuscript U(r,t) in the orientation used by NoHiddenCrossingU.

Equations

• GerverSofa.PartC.Stage2.UValue r t = GerverSofa.dot (GerverSofa.Romik.path GerverSofa.PartC.params r - GerverSofa.Romik.path GerverSofa.PartC.params t) (GerverSofa.u t)

noncomputable def GerverSofa.PartC.Stage2.VValue (t r : ℝ) : ℝ

Reflected manuscript V(t,r).

Equations

• GerverSofa.PartC.Stage2.VValue t r = GerverSofa.dot (GerverSofa.Romik.path GerverSofa.PartC.params r - GerverSofa.Romik.path GerverSofa.PartC.params t) (GerverSofa.v t)

C10: source-clean phase derivative identities — residual batch fix

This revision keeps the C09 no-convert architecture and fixes the complete residual class from the C09 clean build. It uses eta-expanded derivative combinators (fun_add, fun_sub, fun_mul, fun_neg, fun_smul) so the function carried by HasDerivAt is in the desired shape from the start. The proof remains organized in body coordinates and the accompanying runner forces a fresh build of this module.

noncomputable def GerverSofa.PartC.Stage2.phaseA1 (t : ℝ) : Point

Phase-local outer A contact, written in vector form.

Equations

• GerverSofa.PartC.Stage2.phaseA1 t = GerverSofa.Romik.path1 GerverSofa.PartC.params t + (GerverSofa.Romik.alphaBeta1 GerverSofa.PartC.params t).1 • GerverSofa.v t + GerverSofa.u t

noncomputable def GerverSofa.PartC.Stage2.phaseA2 (t : ℝ) : Point

The phase 2 formula for the outer A contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseA2 t = GerverSofa.Romik.path2 GerverSofa.PartC.params t + (GerverSofa.Romik.alphaBeta2 GerverSofa.PartC.params t).1 • GerverSofa.v t + GerverSofa.u t

noncomputable def GerverSofa.PartC.Stage2.phaseA3 (t : ℝ) : Point

The phase 3 formula for the outer A contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseA3 t = GerverSofa.Romik.path3 GerverSofa.PartC.params t + (GerverSofa.Romik.alphaBeta3 GerverSofa.PartC.params t).1 • GerverSofa.v t + GerverSofa.u t

noncomputable def GerverSofa.PartC.Stage2.phaseA4 (t : ℝ) : Point

The phase 4 formula for the outer A contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseA4 t = GerverSofa.Romik.path4 GerverSofa.PartC.params t + (GerverSofa.Romik.alphaBeta4 GerverSofa.PartC.params t).1 • GerverSofa.v t + GerverSofa.u t

noncomputable def GerverSofa.PartC.Stage2.phaseA5 (t : ℝ) : Point

The phase 5 formula for the outer A contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseA5 t = GerverSofa.Romik.path5 GerverSofa.PartC.params t + (GerverSofa.Romik.alphaBeta5 GerverSofa.PartC.params t).1 • GerverSofa.v t + GerverSofa.u t

noncomputable def GerverSofa.PartC.Stage2.phaseC1 (t : ℝ) : Point

Phase-local outer C contact, written in vector form.

Equations

• GerverSofa.PartC.Stage2.phaseC1 t = GerverSofa.Romik.path1 GerverSofa.PartC.params t - (GerverSofa.Romik.alphaBeta1 GerverSofa.PartC.params t).2 • GerverSofa.u t + GerverSofa.v t

noncomputable def GerverSofa.PartC.Stage2.phaseC2 (t : ℝ) : Point

The phase 2 formula for the outer C contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseC2 t = GerverSofa.Romik.path2 GerverSofa.PartC.params t - (GerverSofa.Romik.alphaBeta2 GerverSofa.PartC.params t).2 • GerverSofa.u t + GerverSofa.v t

noncomputable def GerverSofa.PartC.Stage2.phaseC3 (t : ℝ) : Point

The phase 3 formula for the outer C contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseC3 t = GerverSofa.Romik.path3 GerverSofa.PartC.params t - (GerverSofa.Romik.alphaBeta3 GerverSofa.PartC.params t).2 • GerverSofa.u t + GerverSofa.v t

noncomputable def GerverSofa.PartC.Stage2.phaseC4 (t : ℝ) : Point

The phase 4 formula for the outer C contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseC4 t = GerverSofa.Romik.path4 GerverSofa.PartC.params t - (GerverSofa.Romik.alphaBeta4 GerverSofa.PartC.params t).2 • GerverSofa.u t + GerverSofa.v t

noncomputable def GerverSofa.PartC.Stage2.phaseC5 (t : ℝ) : Point

The phase 5 formula for the outer C contact curve.

Equations

• GerverSofa.PartC.Stage2.phaseC5 t = GerverSofa.Romik.path5 GerverSofa.PartC.params t - (GerverSofa.Romik.alphaBeta5 GerverSofa.PartC.params t).2 • GerverSofa.u t + GerverSofa.v t

noncomputable def GerverSofa.PartC.Stage2.vecA (r t : ℝ) : Point

The vertical frame vector scaled by the contact coefficient r.

Equations

• GerverSofa.PartC.Stage2.vecA r t = (-r * Real.sin t, r * Real.cos t)

noncomputable def GerverSofa.PartC.Stage2.vecC (r t : ℝ) : Point

The negative horizontal frame vector scaled by the contact coefficient r.

Equations

• GerverSofa.PartC.Stage2.vecC r t = (-r * Real.cos t, -r * Real.sin t)

theorem GerverSofa.PartC.Stage2.square_hasDerivAt (t : ℝ) : HasDerivAt (fun (s : ℝ) => s * s) (t + t) t

Derivative of the scalar square in the additive form used by the phase formulas.

theorem GerverSofa.PartC.Stage2.u_hasDerivAt (t : ℝ) : HasDerivAt u (v t) t

The horizontal frame vector has derivative equal to the vertical frame vector.

theorem GerverSofa.PartC.Stage2.v_hasDerivAt (t : ℝ) : HasDerivAt v (-u t) t

The vertical frame vector has derivative equal to the negative horizontal vector.

theorem GerverSofa.PartC.Stage2.rotAddK_hasDerivAt {z1 z2 : ℝ → ℝ} {z1' z2' k1 k2 : ℝ} (t : ℝ) (hz1 : HasDerivAt z1 z1' t) (hz2 : HasDerivAt z2 z2' t) : HasDerivAt (fun (s : ℝ) => Romik.addK (Romik.rot s (z1 s, z2 s)) k1 k2) (Romik.rot t (z1' - z2 t, z2' + z1 t)) t

Derivative of addK (rot t (z1 t,z2 t)) in body coordinates.

theorem GerverSofa.PartC.Stage2.path1_hasDerivAt (t : ℝ) : HasDerivAt (Romik.path1 params) (Romik.rot t (Romik.alphaBeta1 params t)) t

The phase 1 path has the specified velocity in the rotating frame.

theorem GerverSofa.PartC.Stage2.path2_hasDerivAt (t : ℝ) : HasDerivAt (Romik.path2 params) (Romik.rot t (Romik.alphaBeta2 params t)) t

The phase 2 path has the specified velocity in the rotating frame.

theorem GerverSofa.PartC.Stage2.path3_hasDerivAt (t : ℝ) : HasDerivAt (Romik.path3 params) (Romik.rot t (Romik.alphaBeta3 params t)) t

The phase 3 path has the specified velocity in the rotating frame.

theorem GerverSofa.PartC.Stage2.path4_hasDerivAt (t : ℝ) : HasDerivAt (Romik.path4 params) (Romik.rot t (Romik.alphaBeta4 params t)) t

The phase 4 path has the specified velocity in the rotating frame.

theorem GerverSofa.PartC.Stage2.path5_hasDerivAt (t : ℝ) : HasDerivAt (Romik.path5 params) (Romik.rot t (Romik.alphaBeta5 params t)) t

The phase 5 path has the specified velocity in the rotating frame.

theorem GerverSofa.PartC.Stage2.A1_hasDerivAt (t : ℝ) : HasDerivAt phaseA1 (vecA 0 t) t

Phase 1: A' = 0 * v.

theorem GerverSofa.PartC.Stage2.A2_hasDerivAt (t : ℝ) : HasDerivAt phaseA2 (vecA (-(1 / 4) * t * t + params.b1 * t + params.b2 + 1 / 2) t) t

Phase 2: A' = beta_2 * v.

theorem GerverSofa.PartC.Stage2.A3_hasDerivAt (t : ℝ) : HasDerivAt phaseA3 (vecA (1 + params.c1 - t) t) t

Phase 3: A' = beta_3 * v.

theorem GerverSofa.PartC.Stage2.A4_hasDerivAt (t : ℝ) : HasDerivAt phaseA4 (vecA (params.d1 - t / 2) t) t

Phase 4: A' = (d1-t/2) * v.

theorem GerverSofa.PartC.Stage2.A5_hasDerivAt (t : ℝ) : HasDerivAt phaseA5 (vecA (1 / 2) t) t

Phase 5: A' = (1/2) * v.

theorem GerverSofa.PartC.Stage2.C1_hasDerivAt (t : ℝ) : HasDerivAt phaseC1 (vecC (1 / 2) t) t

Phase 1: C' = -(1/2) * u.

theorem GerverSofa.PartC.Stage2.C2_hasDerivAt (t : ℝ) : HasDerivAt phaseC2 (vecC (t / 2 - params.b1) t) t

Phase 2: C' = -(t/2-b1) * u.

theorem GerverSofa.PartC.Stage2.C3_hasDerivAt (t : ℝ) : HasDerivAt phaseC3 (vecC (1 + params.c2 + t) t) t

Phase 3: C' = -(1+c2+t) * u.

theorem GerverSofa.PartC.Stage2.C4_hasDerivAt (t : ℝ) : HasDerivAt phaseC4 (vecC (-(1 / 4) * t * t + params.d1 * t + params.d2 + 1 / 2) t) t

Phase 4: C' = -rhoC_4 * u.

theorem GerverSofa.PartC.Stage2.C5_hasDerivAt (t : ℝ) : HasDerivAt phaseC5 (vecC 0 t) t

Phase 5: C' = 0 * u.

Public derivative shapes for downstream Part C closure

The source-clean phase proofs above use private vecA/vecC helpers. These public lemmas expose exactly the stable geometric derivative shapes used by the direct support proof. The transport is derivative-only: the function itself is unchanged, and the remaining pair equality is elementary algebra.

theorem GerverSofa.PartC.Stage2.A1_hasDerivAt_public (t : ℝ) : HasDerivAt phaseA1 (0 • v t) t

theorem GerverSofa.PartC.Stage2.A2_hasDerivAt_public (t : ℝ) : HasDerivAt phaseA2 ((-(1 / 4) * t * t + params.b1 * t + params.b2 + 1 / 2) • v t) t

theorem GerverSofa.PartC.Stage2.A3_hasDerivAt_public (t : ℝ) : HasDerivAt phaseA3 ((1 + params.c1 - t) • v t) t

theorem GerverSofa.PartC.Stage2.A4_hasDerivAt_public (t : ℝ) : HasDerivAt phaseA4 ((params.d1 - t / 2) • v t) t

theorem GerverSofa.PartC.Stage2.A5_hasDerivAt_public (t : ℝ) : HasDerivAt phaseA5 ((1 / 2) • v t) t

theorem GerverSofa.PartC.Stage2.C1_hasDerivAt_public (t : ℝ) : HasDerivAt phaseC1 (-(1 / 2) • u t) t

theorem GerverSofa.PartC.Stage2.C2_hasDerivAt_public (t : ℝ) : HasDerivAt phaseC2 (-(t / 2 - params.b1) • u t) t

theorem GerverSofa.PartC.Stage2.C3_hasDerivAt_public (t : ℝ) : HasDerivAt phaseC3 (-(1 + params.c2 + t) • u t) t

theorem GerverSofa.PartC.Stage2.C4_hasDerivAt_public (t : ℝ) : HasDerivAt phaseC4 (-(-(1 / 4) * t * t + params.d1 * t + params.d2 + 1 / 2) • u t) t

theorem GerverSofa.PartC.Stage2.C5_hasDerivAt_public (t : ℝ) : HasDerivAt phaseC5 (0 • u t) t

Direct outer-support closure for Part C

This proof uses the five source-clean phase derivative identities and glues monotonicity across the four certified switching times. It does not require a globally differentiable contact parametrisation at the speed-change junctions.

theorem GerverSofa.PartC.Stage3.rot_dot_u (t : ℝ) (z : Point) : dot (Romik.rot t z) (u t) = z.1

The horizontal rotating-frame projection recovers the first body coordinate.

theorem GerverSofa.PartC.Stage3.rot_dot_v (t : ℝ) (z : Point) : dot (Romik.rot t z) (v t) = z.2

The vertical rotating-frame projection recovers the second body coordinate.

theorem GerverSofa.PartC.Stage3.rot_injective (t : ℝ) : Function.Injective (Romik.rot t)

Rotation in body coordinates is injective.

theorem GerverSofa.PartC.Stage3.A_own_max (s : ℝ) (hs : s ∈ Set.Icc 0 T) (t : ℝ) : t ∈ Set.Icc 0 T → dot (A t) (u s) ≤ dot (A s) (u s)

theorem GerverSofa.PartC.Stage3.C_own_max (s : ℝ) (hs : s ∈ Set.Icc 0 T) (t : ℝ) : t ∈ Set.Icc 0 T → dot (C t) (v s) ≤ dot (C s) (v s)

theorem GerverSofa.PartC.Stage3.A_base_nonneg (t : ℝ) : t ∈ Set.Icc 0 T → 0 ≤ (A t).2

theorem GerverSofa.PartC.Stage3.C_base_nonneg (t : ℝ) : t ∈ Set.Icc 0 T → 0 ≤ (C t).2

theorem GerverSofa.PartC.Stage3.supportA_direct (t : ℝ) : t ∈ Set.Icc 0 T → A t ∈ K

theorem GerverSofa.PartC.Stage3.supportC_direct (t : ℝ) : t ∈ Set.Icc 0 T → C t ∈ K

Part C direct final assembly

This module bypasses the earlier conditional calculus/branch certificate layers. The two outer-support fields are now concrete theorems. What remains here is exactly the six substantive topology/no-hidden facts; no additional certificate wrapper is introduced.

theorem GerverSofa.PartC.Stage3.globalGeometryDirect (hU : NoHiddenCrossingU) (hV : NoHiddenCrossingV) (hboundary : frontier (Romik.niche params) = claimedNicheBoundary) (hniche : IsConnected (Romik.niche params)) (hanchor : anchor ∈ G) (hG : IsConnected G) : GlobalGeometryCertificate

Direct global geometry from the concrete support proof and the six exact remaining topology/no-hidden statements.

Part C Stage 4: public path differential layer

Source-clean phase derivatives of the five Gerver path pieces. These are provided here as compatibility wrappers around the shared Stage 2 proofs.

theorem GerverSofa.PartC.Stage4.path1_hasDerivAt_public (t : ℝ) : HasDerivAt (Romik.path1 params) (Romik.rot t (Romik.alphaBeta1 params t)) t

theorem GerverSofa.PartC.Stage4.path2_hasDerivAt_public (t : ℝ) : HasDerivAt (Romik.path2 params) (Romik.rot t (Romik.alphaBeta2 params t)) t

theorem GerverSofa.PartC.Stage4.path3_hasDerivAt_public (t : ℝ) : HasDerivAt (Romik.path3 params) (Romik.rot t (Romik.alphaBeta3 params t)) t

theorem GerverSofa.PartC.Stage4.path4_hasDerivAt_public (t : ℝ) : HasDerivAt (Romik.path4 params) (Romik.rot t (Romik.alphaBeta4 params t)) t

theorem GerverSofa.PartC.Stage4.path5_hasDerivAt_public (t : ℝ) : HasDerivAt (Romik.path5 params) (Romik.rot t (Romik.alphaBeta5 params t)) t

The five public phase derivative theorems above are the complete differential interface used by Stage 4. We intentionally do not assert a global HasDerivAt for the nested-if path at switching times: such a theorem requires a separate matching-of-derivatives argument and is neither needed nor used by the Part C closure.

Part C Stage 4: concrete geometry facts

C21: source-clean root closure. In particular, branch decisions for the literal nested-if path are made before endpoint abbreviations are unfolded. The core-path nonnegativity statement is transported from the already sound Part B cell enclosure instead of being reproved by a large transcendental nlinarith call.

theorem GerverSofa.PartC.Stage4.phi_pos : 0 < params.phi

theorem GerverSofa.PartC.Stage4.phi_lt_theta : params.phi < params.theta

theorem GerverSofa.PartC.Stage4.theta_pos : 0 < params.theta

theorem GerverSofa.PartC.Stage4.theta_lt_eta : params.theta < eta

theorem GerverSofa.PartC.Stage4.eta_lt_tau : eta < tau

theorem GerverSofa.PartC.Stage4.eta_lt_T : eta < T

theorem GerverSofa.PartC.Stage4.tau_lt_T : tau < T

theorem GerverSofa.PartC.Stage4.theta_lt_T : params.theta < T

theorem GerverSofa.PartC.Stage4.phi_lt_T : params.phi < T

theorem GerverSofa.PartC.Stage4.phi_lt_eta : params.phi < eta

theorem GerverSofa.PartC.Stage4.theta_lt_tau : params.theta < tau

C23: minimal exact reflection bridge

C22 tried to replace the whole scalar layer at once and regressed badly. C23 rolls back to the stable C21 file and cherry-picks only the reflection bridge needed for D_theta_eq_path_tau.

theorem GerverSofa.PartC.Stage4.B_eta_eq_path_phi : B eta = Romik.path params params.phi

Equation pair 20--21 is exactly the first niche contact.

theorem GerverSofa.PartC.Stage4.D_theta_eq_path_tau : D params.theta = Romik.path params tau

Reflected contact at the other end of the core.

theorem GerverSofa.PartC.Stage4.B_T_y_zero : (B T).2 = 0

The two base endpoints of the claimed niche boundary lie on y=0.

theorem GerverSofa.PartC.Stage4.D_zero_y_zero : (D 0).2 = 0

Exact mesh transport for the literal core path. Cells 1--62 are uniformly above the base. Cells 0 and 63 are intentionally excluded: their interval hulls contain the terminal base contacts and have a tiny negative lower hull.

C30 strengthens the already kernel-checked cell statement from nonnegativity to strict positivity on every core cell. The computation is the same finite exact-rational decision problem; only the target relation is stronger.

theorem GerverSofa.PartC.Stage4.B_eta_y_pos : 0 < (B eta).2

The first core contact is strictly above the base.

theorem GerverSofa.PartC.Stage4.D_theta_y_pos : 0 < (D params.theta).2

The reflected core contact has the same strictly positive height.

theorem GerverSofa.PartC.Stage4.path_core_y_nonneg {t : ℝ} (ht : t ∈ Set.Icc params.phi tau) : 0 ≤ (Romik.path params t).2

Nonnegativity of the literal Gerver path on the core interval, transported from the already proved Part B interval semantics.

theorem GerverSofa.PartC.Stage4.path_core_y_pos {t : ℝ} (ht : t ∈ Set.Icc params.phi tau) : 0 < (Romik.path params t).2

Strict positivity of the literal Gerver path height on the complete core interval [phi,tau]. C30 transports the exact strict lower hull proved above through the existing Part B interval-containment theorem.

A compact phase-2 lower bound for the reflected contact D. It is also used, by the exact phase-2/phase-4 reflection, to control the late B arc.

theorem GerverSofa.PartC.Stage4.D_y_nonneg {t : ℝ} (ht : t ∈ Set.Icc 0 params.theta) : 0 ≤ (D t).2

Nonnegative height of the reflected early contact arc.

theorem GerverSofa.PartC.Stage4.B_y_nonneg {t : ℝ} (ht : t ∈ Set.Icc eta T) : 0 ≤ (B t).2

Nonnegative height of the reflected late contact arc.

C31: strict positivity on the two open contact tails. The base endpoints D 0 and B T have height exactly zero, so the natural domains are Ioc and Ico. These statements are used only for topology of the strict vertical fills; the existing closed-interval nonnegativity theorems remain unchanged.

theorem GerverSofa.PartC.Stage4.D_y_pos {t : ℝ} (ht : t ∈ Set.Ioc 0 params.theta) : 0 < (D t).2

Strict height of the early reflected contact arc away from its base endpoint.

theorem GerverSofa.PartC.Stage4.B_y_pos {t : ℝ} (ht : t ∈ Set.Ico eta T) : 0 < (B t).2

Strict height of the late contact arc away from its base endpoint.

C24: fixed-endpoint separation by a phase-2 Taylor bound and contact monotonicity

C23 reduced the root gate to four scalar U(phi,t) residuals. This replacement removes the large raw nlinarith calls. Phase 2 is reduced to one variable d=t-phi and certified by low-order alternating Taylor bounds. Phases 3--5 use the exact contact identity B(eta)=path(phi) and the sign of the derivative of the phase-local B contact projected on the fixed normal u(t).

theorem GerverSofa.PartC.Stage4.U_phi_nonneg {t : ℝ} (ht : t ∈ Set.Icc params.phi T) : 0 ≤ Stage2.UValue params.phi t

Fixed-endpoint separation required by the direct no-hidden-crossing proof.

Gerver Sofa / Kernel Only / Part C / Stage4 / No Hidden Match Facts

def GerverSofa.PartC.Stage4.noHiddenReflAB (z : Point) : Point

Reflection on the (alpha,beta) coefficient plane induced by t ↦ T-t.

Equations

• GerverSofa.PartC.Stage4.noHiddenReflAB z = (-z.2, -z.1)

theorem GerverSofa.PartC.Stage4.alphaBeta_match12_direct : Romik.alphaBeta1 params params.phi = Romik.alphaBeta2 params params.phi

Exact matching of the coefficient pair at the first switch.

theorem GerverSofa.PartC.Stage4.alphaBeta_match23_direct : Romik.alphaBeta2 params params.theta = Romik.alphaBeta3 params params.theta

Exact matching of the coefficient pair at the second switch.

theorem GerverSofa.PartC.Stage4.alphaBeta4_reflect2_direct (s : ℝ) : Romik.alphaBeta4 params (T - s) = noHiddenReflAB (Romik.alphaBeta2 params s)

Phase four is the reflected phase two coefficient pair.

theorem GerverSofa.PartC.Stage4.alphaBeta3_reflect_direct (s : ℝ) : Romik.alphaBeta3 params (T - s) = noHiddenReflAB (Romik.alphaBeta3 params s)

Phase three has the same coefficient reflection symmetry.

theorem GerverSofa.PartC.Stage4.alphaBeta5_reflect1_direct (s : ℝ) : Romik.alphaBeta5 params (T - s) = noHiddenReflAB (Romik.alphaBeta1 params s)

Phase five is the reflected phase one coefficient pair.

theorem GerverSofa.PartC.Stage4.alphaBeta_match34_direct : Romik.alphaBeta3 params eta = Romik.alphaBeta4 params eta

Exact matching of the coefficient pair at the third switch.

theorem GerverSofa.PartC.Stage4.alphaBeta_match45_direct : Romik.alphaBeta4 params tau = Romik.alphaBeta5 params tau

Exact matching of the coefficient pair at the fourth switch.

Part C Stage 4: continuity of the matched velocity coefficients

This file turns the five exact coefficient matching statements into a public continuity interface for alphaBetaAt, alpha, beta, B, and D.

theorem GerverSofa.PartC.Stage4.alphaBetaAt_continuous : Continuous alphaBetaAt

The literal nested-if velocity coefficient is continuous across all four switches.

theorem GerverSofa.PartC.Stage4.alpha_continuous : Continuous alpha

theorem GerverSofa.PartC.Stage4.beta_continuous : Continuous beta

theorem GerverSofa.PartC.Stage4.D_continuous : Continuous D

Public continuity of the early reflected contact curve.

theorem GerverSofa.PartC.Stage4.B_continuous : Continuous B

Public continuity of the late reflected contact curve.

Gerver Sofa / Kernel Only / Part C / Stage4 / No Hidden Sign Facts

theorem GerverSofa.PartC.Stage4.alpha_nonpos {t : ℝ} (ht : t ∈ Set.Icc params.phi T) : alpha t ≤ 0

The u_t coefficient of the Gerver velocity is nonpositive on the entire no-hidden U domain.

theorem GerverSofa.PartC.Stage4.beta_nonneg {t : ℝ} (ht : t ∈ Set.Icc params.phi T) : 0 ≤ beta t

The v_t coefficient of the Gerver velocity is nonnegative on the entire no-hidden U domain.

Part C Stage 4: positive turning determinant on phases 2--5

The determinant is the signed turning numerator of the nonzero path velocity. These phasewise facts are the analytic input for the remaining one-turn chord argument; they do not assert the no-hidden conclusion by themselves.

The next six statements expose the coefficient-derivative signs used in the manuscript's tangent-angle argument. They are deliberately stated for the explicit smooth-phase formulae; no derivative is assigned at a switch.

theorem GerverSofa.PartC.Stage4.phase2_betaPrime_neg {r : ℝ} (hr : r ∈ Set.Ioo params.phi params.theta) : -(1 / 2) * r + params.b1 < 0

theorem GerverSofa.PartC.Stage4.phase4_alphaPrime_neg {r : ℝ} (hr : r ∈ Set.Ioo eta tau) : 1 / 2 * r - params.d1 < 0

theorem GerverSofa.PartC.Stage4.phase5_coefficientPrime_nonpos {t : ℝ} (ht : t ∈ Set.Ioo tau T) : -2 * params.e1 * Real.cos t - 2 * params.e2 * Real.sin t ≤ 0 ∧ -2 * params.e1 * Real.sin t + 2 * params.e2 * Real.cos t ≤ 0

Phase-five coefficient derivatives are nonpositive. This is the exact formula-level input used below; strict turning follows from the strict nonvanishing of the first coefficient.

Part C Stage 4: global path derivative and one-turn velocity monotonicity

The path derivative is glued across the four switches using equality of both the path values and the body-frame velocity coefficients. The coefficient derivatives themselves need not match at a switch. Consequently the fixed projection is proved antitone phase by phase and then glued order-theoretically.

theorem GerverSofa.PartC.Stage4.path_hasDerivAt_noHidden (x : ℝ) : HasDerivAt (Romik.path params) (Romik.rot x (alphaBetaAt x)) x

The literal five-piece Gerver path is differentiable at the switches as well as in the phase interiors.

noncomputable def GerverSofa.PartC.Stage4.uVelocity (t r : ℝ) : ℝ

Scalar projection of the corner velocity on the fixed vector u(t).

Equations

• GerverSofa.PartC.Stage4.uVelocity t r = GerverSofa.PartC.alpha r * Real.cos (t - r) + GerverSofa.PartC.beta r * Real.sin (t - r)

theorem GerverSofa.PartC.Stage4.uVelocity_antitone {t : ℝ} (ht : t ∈ Set.Icc params.phi T) : AntitoneOn (uVelocity t) (Set.Icc params.phi t)

For fixed terminal time, the projected path velocity is antitone on the complete ordered no-hidden interval.

theorem GerverSofa.PartC.Stage4.UValue_hasDerivAt_noHidden (r t : ℝ) : HasDerivAt (fun (s : ℝ) => Stage2.UValue s t) (uVelocity t r) r

Derivative of U(r,t) in its first variable.

theorem GerverSofa.PartC.Stage4.U_concave_on (t : ℝ) (ht : t ∈ Set.Icc params.phi T) : ConcaveOn ℝ (Set.Icc params.phi t) fun (r : ℝ) => Stage2.UValue r t

Concavity form of the manuscript's one-turn tangent argument.

Part C Stage 4: exact reflection bridge for the second no-hidden inequality

The affine reflection is derived phase by phase from the certified matching equations. No global symmetry hypothesis is introduced.

noncomputable def GerverSofa.PartC.Stage4.noHiddenHReflect (z : Point) : Point

Reflect a point horizontally about the axis x = k31.

Equations

• GerverSofa.PartC.Stage4.noHiddenHReflect z = (2 * GerverSofa.PartC.params.k31 - z.1, z.2)

@[simp]

theorem GerverSofa.PartC.Stage4.noHiddenHReflect_involutive (z : Point) : noHiddenHReflect (noHiddenHReflect z) = z

theorem GerverSofa.PartC.Stage4.path_reflect_noHidden {s : ℝ} (hs : s ∈ Set.Icc 0 T) : Romik.path params (T - s) = noHiddenHReflect (Romik.path params s)

Exact global horizontal reflection of the literal five-piece path.

theorem GerverSofa.PartC.Stage4.VValue_eq_reflected_UValue {t r : ℝ} (ht : t ∈ Set.Icc 0 T) (hr : r ∈ Set.Icc 0 T) : Stage2.VValue t r = Stage2.UValue (T - r) (T - t)

Reflection transports the second no-hidden scalar to the first one.

Part C Stage 4: direct no-hidden-crossing closure

The first inequality follows from concavity and the two endpoint values. The second is its exact phase-derived horizontal reflection.

theorem GerverSofa.PartC.Stage4.noHiddenU_direct : NoHiddenCrossingU

Concrete first no-hidden-crossing theorem.

theorem GerverSofa.PartC.Stage4.noHiddenV_direct : NoHiddenCrossingV

Concrete reflected no-hidden-crossing theorem.

Gerver Sofa / Kernel Only / Part C / Stage4 / Niche Envelope Support

theorem GerverSofa.PartC.Stage4.early_endpoint_diagonal_nonneg {t : ℝ} (ht : t ∈ Set.Icc 0 params.phi) : 0 ≤ dot (Romik.path params params.phi - Romik.path params t) (u t + v t)

theorem GerverSofa.PartC.Stage4.B_early_diagonal_nonneg {t r : ℝ} (ht : t ∈ Set.Icc 0 params.phi) (hr : r ∈ Set.Icc eta T) : 0 ≤ dot (B r - Romik.path params t) (u t + v t)

theorem GerverSofa.PartC.Stage4.B_early_boundary_outside {t r : ℝ} (ht : t ∈ Set.Icc 0 params.phi) (hr : r ∈ Set.Icc eta T) : 0 ≤ dot (B r - Romik.path params t) (u t) ∨ 0 ≤ dot (B r - Romik.path params t) (v t)

theorem GerverSofa.PartC.Stage4.B_late_u_nonneg {t r : ℝ} (ht : t ∈ Set.Icc params.phi T) (hr : r ∈ Set.Icc eta T) : 0 ≤ dot (B r - Romik.path params t) (u t)

theorem GerverSofa.PartC.Stage4.B_boundary_outside {t r : ℝ} (ht : t ∈ Set.Ioo 0 T) (hr : r ∈ Set.Icc eta T) : 0 ≤ dot (B r - Romik.path params t) (u t) ∨ 0 ≤ dot (B r - Romik.path params t) (v t)

theorem GerverSofa.PartC.Stage4.B_T_u_nonneg_early {t : ℝ} (ht : t ∈ Set.Icc 0 params.phi) : 0 ≤ dot (B T - Romik.path params t) (u t)

theorem GerverSofa.PartC.Stage4.B_T_u_nonneg {t : ℝ} (ht : t ∈ Set.Ioo 0 T) : 0 ≤ dot (B T - Romik.path params t) (u t)

Exact reflected forms

Only the early half of the coefficient reflection is needed here. Its image under r ↦ T-r is exactly the late B interval. Keeping the endpoint cases explicit avoids relying on definitional reduction across the four switching equalities of alphaBetaAt.

theorem GerverSofa.PartC.Stage4.B_reflect_D {r : ℝ} (hr : r ∈ Set.Icc 0 params.theta) : B (T - r) = noHiddenHReflect (D r)

The late B contact arc is the exact horizontal reflection of the early D contact arc.

theorem GerverSofa.PartC.Stage4.D_boundary_outside {t r : ℝ} (ht : t ∈ Set.Ioo 0 T) (hr : r ∈ Set.Icc 0 params.theta) : 0 ≤ dot (D r - Romik.path params t) (u t) ∨ 0 ≤ dot (D r - Romik.path params t) (v t)

Every point of the early D contact arc lies outside at least one of the two moving inner walls.

theorem GerverSofa.PartC.Stage4.D_zero_v_nonneg {t : ℝ} (ht : t ∈ Set.Ioo 0 T) : 0 ≤ dot (D 0 - Romik.path params t) (v t)

Reflected endpoint separator used for the strict lower horizontal range of the niche.

Part C Stage 4: independent cap convexity and anchor foundation

This module separates the already direct cap geometry from the later theorem that removing the downward niche preserves connectedness.

theorem GerverSofa.PartC.Stage4.anchor_mem_K_direct : anchor ∈ K

The concrete endpoint anchor belongs to the reconstructed cap.

theorem GerverSofa.PartC.Stage4.K_convex_direct : Convex ℝ K

Convexity of the literal cap follows directly from its half-plane definition.

theorem GerverSofa.PartC.Stage4.K_connected_direct : IsConnected K

The nonempty convex cap is connected.

Part C Stage 4: independent vertical-fill topology

This module isolates the connectedness half of the niche argument from the upper-envelope/frontier equality. It can therefore be kernel-built even while the boundary module is still under repair.

def GerverSofa.PartC.Stage4.verticalFill (f : ℝ → Point) (I : Set ℝ) : Set Point

Vertical fill below a parametrized graph.

Equations

• GerverSofa.PartC.Stage4.verticalFill f I = {q : GerverSofa.Point | ∃ t ∈ I, q.1 = (f t).1 ∧ 0 ≤ q.2 ∧ q.2 < (f t).2}

def GerverSofa.PartC.Stage4.certifiedNicheRegion : Set Point

The three certified upper-envelope pieces as strict vertical fills.

Equations

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

theorem GerverSofa.PartC.Stage4.niche_piece_endpoints : B eta = Romik.path params params.phi ∧ D params.theta = Romik.path params tau ∧ (B T).2 = 0 ∧ (D 0).2 = 0

Consecutive endpoint incidences of the three graph pieces.

theorem GerverSofa.PartC.Stage4.verticalFill_strict_isConnected {f : ℝ → Point} {I : Set ℝ} (hI : IsConnected I) (hf : ContinuousOn f I) (hy : ∀ t ∈ I, 0 < (f t).2) : IsConnected (verticalFill f I)

A strict positive vertical fill is a continuous image of a connected product.

theorem GerverSofa.PartC.Stage4.D_fill_Icc_eq_Ioc : verticalFill D (Set.Icc 0 params.theta) = verticalFill D (Set.Ioc 0 params.theta)

theorem GerverSofa.PartC.Stage4.B_fill_Icc_eq_Ico : verticalFill B (Set.Icc eta T) = verticalFill B (Set.Ico eta T)

theorem GerverSofa.PartC.Stage4.niche_fills_overlap : (verticalFill D (Set.Ioc 0 params.theta) ∩ verticalFill (Romik.path params) (Set.Icc params.phi tau)).Nonempty ∧ (verticalFill (Romik.path params) (Set.Icc params.phi tau) ∩ verticalFill B (Set.Ico eta T)).Nonempty

theorem GerverSofa.PartC.Stage4.certifiedNicheRegion_connected : IsConnected certifiedNicheRegion

Connectedness of the certified three-piece vertical-fill region.

Part C Stage 4: inner-wall graph identities

noncomputable def GerverSofa.PartC.Stage4.bRoof (t X : ℝ) : ℝ

First inner wall as a graph over horizontal coordinate.

Equations

• GerverSofa.PartC.Stage4.bRoof t X = (GerverSofa.dot (GerverSofa.Romik.path GerverSofa.PartC.params t) (GerverSofa.u t) - X * Real.cos t) / Real.sin t

noncomputable def GerverSofa.PartC.Stage4.dRoof (t X : ℝ) : ℝ

Second inner wall as a graph over horizontal coordinate.

Equations

• GerverSofa.PartC.Stage4.dRoof t X = (GerverSofa.dot (GerverSofa.Romik.path GerverSofa.PartC.params t) (GerverSofa.v t) + X * Real.sin t) / Real.cos t

noncomputable def GerverSofa.PartC.Stage4.instantRoof (t X : ℝ) : ℝ

Vertical roof of one instantaneous open inner quadrant.

Equations

• GerverSofa.PartC.Stage4.instantRoof t X = min (GerverSofa.PartC.Stage4.bRoof t X) (GerverSofa.PartC.Stage4.dRoof t X)

theorem GerverSofa.PartC.Stage4.mem_innerQuadrant_iff_roofs {t X Y : ℝ} (ht : t ∈ Set.Ioo 0 T) : (X, Y) ∈ Romik.innerQuadrantAt params t ↔ Y < bRoof t X ∧ Y < dRoof t X

A point of nonnegative height is in the instantaneous inner quadrant iff it lies strictly below both graph roofs.

theorem GerverSofa.PartC.Stage4.roofs_at_path (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : bRoof t (Romik.path params t).1 = (Romik.path params t).2 ∧ dRoof t (Romik.path params t).1 = (Romik.path params t).2

The two walls agree at their apex.

Part C Stage 4: direct membership of the certified vertical fills

These are the three concrete reverse-inclusion facts needed to identify the literal niche with its certified vertical-fill region. They are proved from the literal open-quadrant definition, not assumed through a Stage 2 API.

theorem GerverSofa.PartC.Stage4.vertical_below_path_mem_niche {r Y : ℝ} (hr : r ∈ Set.Icc params.phi tau) (hY0 : 0 ≤ Y) (hY : Y < (Romik.path params r).2) : ((Romik.path params r).1, Y) ∈ Romik.niche params

Every strict vertical point below a core-path point belongs to the literal niche.

theorem GerverSofa.PartC.Stage4.vertical_below_B_mem_niche {r Y : ℝ} (hr : r ∈ Set.Icc eta T) (hY0 : 0 ≤ Y) (hY : Y < (B r).2) : ((B r).1, Y) ∈ Romik.niche params

Every strict vertical point below the late B contact belongs to the literal niche.

theorem GerverSofa.PartC.Stage4.vertical_below_D_mem_niche {r Y : ℝ} (hr : r ∈ Set.Icc 0 params.theta) (hY0 : 0 ≤ Y) (hY : Y < (D r).2) : ((D r).1, Y) ∈ Romik.niche params

Every strict vertical point below the early D contact belongs to the literal niche.

Part C Stage 4: frontier of a strict vertical subgraph

This file contains the topological calculation used by the concrete Gerver niche. The generic lemma is intentionally independent of the old Stage 2 topology sketches: it computes the closure and the interior of a strict vertical subgraph directly.

The three Gerver roof arcs are graphs over horizontal position

theorem GerverSofa.PartC.Stage4.D_fst_strictMono : StrictMonoOn (fun (t : ℝ) => (D t).1) (Set.Icc 0 params.theta)

The early contact arc has strictly increasing horizontal projection.

theorem GerverSofa.PartC.Stage4.B_fst_strictMono : StrictMonoOn (fun (t : ℝ) => (B t).1) (Set.Icc eta T)

The late contact arc has strictly increasing horizontal projection.

theorem GerverSofa.PartC.Stage4.core_path_fst_strictAnti : StrictAntiOn (fun (t : ℝ) => (Romik.path params t).1) (Set.Icc params.phi tau)

The core path runs strictly from right to left in horizontal projection.

A single left-to-right parametrization of the three roof arcs

noncomputable def GerverSofa.PartC.Stage4.coreReverseTime (s : ℝ) : ℝ

The affine reversal which runs through the core path from tau to phi while the auxiliary parameter runs from theta to eta.

Equations

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

noncomputable def GerverSofa.PartC.Stage4.nicheTopArc (s : ℝ) : Point

A single continuous parametrization of the complete upper niche arc.

Equations

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

theorem GerverSofa.PartC.Stage4.nicheTopArc_continuous : Continuous nicheTopArc

theorem GerverSofa.PartC.Stage4.nicheTopArc_fst_strictMono : StrictMonoOn (fun (s : ℝ) => (nicheTopArc s).1) (Set.Icc 0 T)

Horizontal projection of the complete upper arc is strictly increasing.

theorem GerverSofa.PartC.Stage4.nicheTopArc_y_nonneg {s : ℝ} (hs : s ∈ Set.Icc 0 T) : 0 ≤ (nicheTopArc s).2

theorem GerverSofa.PartC.Stage4.nicheTopArc_y_pos {s : ℝ} (hs : s ∈ Set.Ioo 0 T) : 0 < (nicheTopArc s).2

theorem GerverSofa.PartC.Stage4.nicheTopArc_zero : nicheTopArc 0 = D 0

theorem GerverSofa.PartC.Stage4.nicheTopArc_T : nicheTopArc T = B T

theorem GerverSofa.PartC.Stage4.coreReverseTime_image : coreReverseTime '' Set.Icc params.theta eta = Set.Icc params.phi tau

theorem GerverSofa.PartC.Stage4.nicheTopArc_image : curveImage nicheTopArc (Set.Icc 0 T) = curveImage D (Set.Icc 0 params.theta) ∪ curveImage (Romik.path params) (Set.Icc params.phi tau) ∪ curveImage B (Set.Icc eta T)

The glued arc has exactly the three curve images, with no additional points introduced by the reparametrization.

def GerverSofa.PartC.Stage4.strictSubgraphRegion (a b : ℝ) (H : ℝ → ℝ) : Set Point

A vertically filled strict subgraph over a compact interval.

Equations

• GerverSofa.PartC.Stage4.strictSubgraphRegion a b H = {p : GerverSofa.Point | p.1 ∈ Set.Icc a b ∧ 0 ≤ p.2 ∧ p.2 < H p.1}

def GerverSofa.PartC.Stage4.closedSubgraphRegion (a b : ℝ) (H : ℝ → ℝ) : Set Point

The closed vertical fill associated with strictSubgraphRegion.

Equations

• GerverSofa.PartC.Stage4.closedSubgraphRegion a b H = {p : GerverSofa.Point | p.1 ∈ Set.Icc a b ∧ 0 ≤ p.2 ∧ p.2 ≤ H p.1}

def GerverSofa.PartC.Stage4.strictSubgraphBoundary (a b : ℝ) (H : ℝ → ℝ) : Set Point

The base together with the graph of the roof.

Equations

• GerverSofa.PartC.Stage4.strictSubgraphBoundary a b H = {p : GerverSofa.Point | p.1 ∈ Set.Icc a b ∧ (p.2 = 0 ∨ p.2 = H p.1)}

theorem GerverSofa.PartC.Stage4.closure_strictSubgraphRegion {a b : ℝ} {H : ℝ → ℝ} (hab : a < b) (hH : Continuous H) (hHnonneg : ∀ x ∈ Set.Icc a b, 0 ≤ H x) (hHpos : ∀ x ∈ Set.Ioo a b, 0 < H x) (ha : H a = 0) (hb : H b = 0) : closure (strictSubgraphRegion a b H) = closedSubgraphRegion a b H

theorem GerverSofa.PartC.Stage4.interior_strictSubgraphRegion {a b : ℝ} {H : ℝ → ℝ} (hH : Continuous H) : interior (strictSubgraphRegion a b H) = {p : Point | p.1 ∈ Set.Ioo a b ∧ 0 < p.2 ∧ p.2 < H p.1}

theorem GerverSofa.PartC.Stage4.frontier_strictSubgraphRegion {a b : ℝ} {H : ℝ → ℝ} (hab : a < b) (hH : Continuous H) (hHnonneg : ∀ x ∈ Set.Icc a b, 0 ≤ H x) (hHpos : ∀ x ∈ Set.Ioo a b, 0 < H x) (ha : H a = 0) (hb : H b = 0) : frontier (strictSubgraphRegion a b H) = strictSubgraphBoundary a b H

The frontier of a positive strict vertical subgraph consists exactly of its roof and its base.

Turning a monotone roof arc into a global continuous graph

noncomputable def GerverSofa.PartC.Stage4.horizontalOrderIso (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : ↑(Set.Icc a b) ≃o ↑(Set.Icc (γ a).1 (γ b).1)

Identify a strictly horizontally increasing arc with its horizontal coordinate interval.

Equations

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

@[simp]

theorem GerverSofa.PartC.Stage4.horizontalOrderIso_apply_val (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) (t : ↑(Set.Icc a b)) : ↑((horizontalOrderIso γ hab hγ hx) t) = (γ ↑t).1

noncomputable def GerverSofa.PartC.Stage4.roofOnHorizontalRange (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : ↑(Set.Icc (γ a).1 (γ b).1) → ℝ

Express the arc’s vertical coordinate as a function of its horizontal coordinate.

Equations

• GerverSofa.PartC.Stage4.roofOnHorizontalRange γ hab hγ hx X = (γ ↑((GerverSofa.PartC.Stage4.horizontalOrderIso γ hab hγ hx).symm X)).2

theorem GerverSofa.PartC.Stage4.continuous_roofOnHorizontalRange (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : Continuous (roofOnHorizontalRange γ hab hγ hx)

theorem GerverSofa.PartC.Stage4.horizontal_endpoints_le (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : (γ a).1 ≤ (γ b).1

noncomputable def GerverSofa.PartC.Stage4.monotoneCurveRoof (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : ℝ → ℝ

Extend the roof graph to the real line by clamping to its endpoint interval.

Equations

• GerverSofa.PartC.Stage4.monotoneCurveRoof γ hab hγ hx = Set.IccExtend ⋯ (GerverSofa.PartC.Stage4.roofOnHorizontalRange γ hab hγ hx)

theorem GerverSofa.PartC.Stage4.continuous_monotoneCurveRoof (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : Continuous (monotoneCurveRoof γ hab hγ hx)

theorem GerverSofa.PartC.Stage4.monotoneCurveRoof_at (γ : ℝ → Point) {a b t : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) (ht : t ∈ Set.Icc a b) : monotoneCurveRoof γ hab hγ hx (γ t).1 = (γ t).2

theorem GerverSofa.PartC.Stage4.verticalFill_eq_strictSubgraphRegion (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : verticalFill γ (Set.Icc a b) = strictSubgraphRegion (γ a).1 (γ b).1 (monotoneCurveRoof γ hab hγ hx)

theorem GerverSofa.PartC.Stage4.curveImage_eq_roofGraph (γ : ℝ → Point) {a b : ℝ} (hab : a < b) (hγ : ContinuousOn γ (Set.Icc a b)) (hx : StrictMonoOn (fun (t : ℝ) => (γ t).1) (Set.Icc a b)) : curveImage γ (Set.Icc a b) = {p : Point | p.1 ∈ Set.Icc (γ a).1 (γ b).1 ∧ p.2 = monotoneCurveRoof γ hab hγ hx p.1}

theorem GerverSofa.PartC.Stage4.T_pos_frontier : 0 < T

noncomputable def GerverSofa.PartC.Stage4.nicheRoof : ℝ → ℝ

The continuous roof function determined by the complete niche top arc.

Equations

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

theorem GerverSofa.PartC.Stage4.nicheRoof_continuous : Continuous nicheRoof

theorem GerverSofa.PartC.Stage4.nicheRoof_at_topArc {s : ℝ} (hs : s ∈ Set.Icc 0 T) : nicheRoof (nicheTopArc s).1 = (nicheTopArc s).2

theorem GerverSofa.PartC.Stage4.nicheRoof_nonneg {X : ℝ} (hX : X ∈ Set.Icc (D 0).1 (B T).1) : 0 ≤ nicheRoof X

theorem GerverSofa.PartC.Stage4.nicheRoof_pos {X : ℝ} (hX : X ∈ Set.Ioo (D 0).1 (B T).1) : 0 < nicheRoof X

theorem GerverSofa.PartC.Stage4.nicheRoof_left : nicheRoof (D 0).1 = 0

theorem GerverSofa.PartC.Stage4.nicheRoof_right : nicheRoof (B T).1 = 0

theorem GerverSofa.PartC.Stage4.certifiedNicheRegion_eq_strictSubgraph : certifiedNicheRegion = strictSubgraphRegion (D 0).1 (B T).1 nicheRoof

The three certified fills form one strict subgraph.

theorem GerverSofa.PartC.Stage4.claimedNicheBoundary_eq_subgraphBoundary : claimedNicheBoundary = strictSubgraphBoundary (D 0).1 (B T).1 nicheRoof

theorem GerverSofa.PartC.Stage4.frontier_certifiedNicheRegion : frontier certifiedNicheRegion = claimedNicheBoundary

Direct frontier calculation for the certified three-fill region.

Literal instantaneous wedges lie below the certified graph

theorem GerverSofa.PartC.Stage4.core_is_upper_envelope {r : ℝ} (hr : r ∈ Set.Icc params.phi tau) (t : ℝ) : t ∈ Set.Ioo 0 T → instantRoof t (Romik.path params r).1 ≤ (Romik.path params r).2

A core path point dominates every instantaneous roof at its horizontal coordinate. This is the exact geometric content of the two no-hidden inequalities.

theorem GerverSofa.PartC.Stage4.nicheTopArc_is_upper_envelope {s t : ℝ} (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Ioo 0 T) : instantRoof t (nicheTopArc s).1 ≤ (nicheTopArc s).2

Every point of the glued certified roof dominates every instantaneous wall roof at its horizontal coordinate.

theorem GerverSofa.PartC.Stage4.niche_eq_certifiedNicheRegion : Romik.niche params = certifiedNicheRegion

Literal niche equals the three concrete strict vertical fills.

theorem GerverSofa.PartC.Stage4.niche_frontier_direct : frontier (Romik.niche params) = claimedNicheBoundary

Final exact set-valued boundary equality required by Part C.

Part C Stage 4: connectedness of the literal niche

The independent vertical-fill module proves connectedness of the certified three-piece region. Once the boundary layer identifies that region with the literal niche, connectedness is immediate.

theorem GerverSofa.PartC.Stage4.niche_connected_direct : IsConnected (Romik.niche params)

Concrete connectedness of the literal niche.

Part C Stage 4: vertical-fibre topology of the fixed sofa

The argument in this file is independent of any Jordan-curve theorem. The cap is compact and convex. Its removed niche is a strict vertical subgraph. Consequently every nonempty vertical section of the complement is an interval. Moreover, a highest point of each cap section survives: if it belonged to the strict subgraph, one of the certified graph points would be a still higher cap point. Thus the horizontal projections of the cap and sofa agree. A compact map with connected fibres over that connected projection closes connectedness.

theorem GerverSofa.PartC.Stage4.beta_nonneg_on_D {t : ℝ} (ht : t ∈ Set.Icc 0 params.theta) : 0 ≤ beta t

The early inner-contact coefficient is nonnegative on the whole D parameter interval.

theorem GerverSofa.PartC.Stage4.core_path_mem_K {t : ℝ} (ht : t ∈ Set.Icc params.phi tau) : Romik.path params t ∈ K

Core path points are cap points.

theorem GerverSofa.PartC.Stage4.D_mem_K {t : ℝ} (ht : t ∈ Set.Icc 0 params.theta) : D t ∈ K

Every certified early D roof point lies in the cap.

theorem GerverSofa.PartC.Stage4.B_mem_K {t : ℝ} (ht : t ∈ Set.Icc eta T) : B t ∈ K

Every certified late B roof point lies in the cap.

theorem GerverSofa.PartC.Stage4.certified_roof_mem_K : (∀ t ∈ Set.Icc 0 params.theta, D t ∈ K) ∧ (∀ t ∈ Set.Icc params.phi tau, Romik.path params t ∈ K) ∧ ∀ t ∈ Set.Icc eta T, B t ∈ K

Every graph which forms the certified strict niche roof consists of cap points.

theorem GerverSofa.PartC.Stage4.verticalFill_downward {f : ℝ → Point} {I : Set ℝ} {p q : Point} (hx : p.1 = q.1) (hp0 : 0 ≤ p.2) (hy : p.2 ≤ q.2) (hq : q ∈ verticalFill f I) : p ∈ verticalFill f I

Strict vertical fills are downward closed along every nonnegative fibre.

theorem GerverSofa.PartC.Stage4.certifiedNicheRegion_downward {p q : Point} (hx : p.1 = q.1) (hp0 : 0 ≤ p.2) (hy : p.2 ≤ q.2) (hq : q ∈ certifiedNicheRegion) : p ∈ certifiedNicheRegion

The union of the three strict graph fills is downward closed in each nonnegative vertical fibre.

theorem GerverSofa.PartC.Stage4.K_compact_direct : IsCompact K

The Gerver cap is compact.

theorem GerverSofa.PartC.Stage4.G_compact_direct : IsCompact G

The fixed sofa is compact, as the difference of the compact cap and the open union of forbidden quadrants.

theorem GerverSofa.PartC.Stage4.exists_G_point_over_K {q : Point} (hq : q ∈ K) : ∃ p ∈ G, p.1 = q.1

Every cap fibre has a highest point, and that point survives removal of the strict niche.

theorem GerverSofa.PartC.Stage4.fst_image_G_eq_fst_image_K : Prod.fst '' G = Prod.fst '' K

Removing the strict niche does not change the horizontal projection.

def GerverSofa.PartC.Stage4.GVerticalSection (x : ℝ) : Set Point

A vertical section of the fixed sofa.

Equations

• GerverSofa.PartC.Stage4.GVerticalSection x = {q : GerverSofa.Point | q ∈ GerverSofa.PartC.G ∧ q.1 = x}

theorem GerverSofa.PartC.Stage4.GVerticalSection_convex (x : ℝ) : Convex ℝ (GVerticalSection x)

Every vertical section of G is convex.

theorem GerverSofa.PartC.Stage4.GVerticalSection_connected {x : ℝ} (hne : (GVerticalSection x).Nonempty) : IsConnected (GVerticalSection x)

Each nonempty vertical section is connected.

theorem GerverSofa.PartC.Stage4.G_connected_by_vertical_fibers : IsConnected G

Connectedness of the fixed Gerver sofa by compact connected fibres.

Part C Stage 4: topology of the concrete fixed set

No new certificate structure is introduced here. This file is intended to close the two literal topology fields left by RemainingTopologyTarget.

theorem GerverSofa.PartC.Stage4.anchor_mem_direct : anchor ∈ G

The left endpoint of the zero-angle support face is the concrete anchor and it is not removed by the niche.

theorem GerverSofa.PartC.Stage4.G_connected_direct : IsConnected G

Direct connectedness of the cap-minus-niche set, obtained from the compact connected horizontal projection and the connected vertical fibres.

Part C final unconditional closure

This is the only terminal assembly for Part C. It contains no payload and no new certificate interface.

theorem GerverSofa.PartC.Stage4.globalGeometryCertificate : GlobalGeometryCertificate

Concrete global geometry certificate.