Documentation

LeanPool.MovingSofa.GerverSofa.KernelOnly.PartE.Certificates.Bundle032

Gerver sofa: related certificate and semantic modules #

Gerver sofa dependency batch #

Intermediate reconstruction of the upper theta cover #

Reconstruction of the upper theta cover #

Gerver Sofa / Kernel Only / Part E / E24KC6Kernel Final Closure #

theorem GerverSofa.PartE.deepMindABPhiTheta_existsUnique :
∃! ABphiTheta : ℝ × ℝ × ℝ × ℝ, DeepMindABPhiThetaSpec ABphiTheta.1 ABphiTheta.2.1 ABphiTheta.2.2.1 ABphiTheta.2.2.2