OAI.RuledApproximation.fullMain
OpenThe theorem states that FullMain holds, which is the conjunction of seven defined statements about covering ruled surfaces in R³ by finitely many infinite cylinders with small total cross-sectional area. A cylinder has a unit axis direction and a base set in the orthogonal complement plane of that axis; it consists of all points b + t·axis with b in the base and t real, and its area is the Lebesgue measure of the base. A finite cover has the cylinders of a prescribed shape (parallelogram, triangle, or open bounded measurable base), with the set contained in their union and the areas summing to at most a given bound. For a field v on the plane, ruled(D,v,L) is the set of points (p₁ + r v₁(p), p₂ + r v₂(p), r) with p in D and |r| ≤ L, and physicalRuled(h,D,v,L) is the set of points (s, p₁ + s v₁(p), h(p₂ + s v₂(p))) with |s| ≤ L. The weights are 1/√(1+‖v‖²) and 1/√(1+w₁²+h²w₂²). HyperbolicAt(L,v,p) means the derivative of v at p has eigenvalues λ and −λ with 0 < Lλ < 1. SmoothNear(n,D,v) means v is C^n on an open neighborhood of D. (1) For compact D, v C¹ near D, L > 0 and hyperbolic at every point of D, for every ε > 0 ruled(D,v,L) has a finite parallelogram cover of total area at most ∫_D 1/√(1+‖v‖²) + ε. (2) With h, L > 0 and the same hypotheses, for every ε > 0 and every isometry F of R³, F applied to physicalRuled(h,D,v,L) has a finite parallelogram cover of area at most h∫_D physicalWeight(h,v) + ε. (3) Logarithmic statement: for X, k > 0, compact D with null boundary, v C² on an open rectangle containing D, and at every point of D zero trace, negative determinant and kX√(−det) < 1 for the derivative of v, physicalRuled(1,D,kv,X) has a finite cover by open bounded measurable-base cylinders of area at most ∫_D 1/√(1+k²‖v‖²) + ε. (4) Product-cell statement: for h, M > 0, compact D with null boundary, v C¹ near D and M-hyperbolic on D, physicalRuled(h,D,v,M) has such an open-bounded cover of area at most h∫_D physicalWeight(h,v) + ε. (5) Orthogonal-grid statement: for compact D with null boundary, v C¹ near D, κ < 1, and at each point zero trace, negative determinant and derivative operator norm at most κ, physicalRuled(√2,D,v,1) has a parallelogram cover of area at most √2∫_D 1/√(1+v₁²+2v₂²) + ε. (6) Nilpotent statement: for compact D and G smooth (C^∞) near D whose derivative squares to zero at every point of D, and any h, ε > 0, there are finitely many square tiles T_i (congruent images of a scaled unit square) and directions g_i such that physicalRuled(1,D,G,1) lies in the union of the auxiliary cylinders {axial(s, b + s g_i)}, the sum of area(T_i)·physicalWeight(h,g_i) is at most ∫_D physicalWeight(h,G) + ε, and for every a there are two families of parallelogram cylinders, whose carriers are the images of these auxiliary cylinders under the two stated coordinate maps (a scaling by h in the third coordinate, and a coordinate swap with reflection a − z₃ scaled by h), each of area h·area(T_i)·physicalWeight(h,g_i). (7) Singular statement: for 1 < p < (√51 − 5)/2 and 1 < γ < 1/(2−p), an explicit coefficient (1/2)⁴(2p²+10p−13)/(30p) is negative, the explicit cost 2·singularCost + 8√2 c^{2γ} equals √2/2 + 2√2·coefficient·c² up to o(c²) as c → 0⁺, and for all sufficiently small c > 0 the regular edge-2 tetrahedron is covered by finitely many parallelogram cylinders covering two singular ruled pieces plus two triangular tip cylinders, with total area less than √2/2.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/RuledCovering.lean; bytes 9682..9723 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_RuledCovering namespace OAI noncomputable section open Set MeasureTheory Filter open scoped Topology ContDiff namespace RuledApproximation
theorem fullMain : FullMain := by sorry end RuledApproximation end end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.