Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

OAI.ComparatorModel.RecursivePotentials.main

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states (its proof is admitted with sorry) that the defined proposition MainClaim holds. MainClaim asserts that there exist constructions, over index types in universe 0, of the finite rooted tree head structure, the tree-vector spaces, the zero-root tree-vector spaces, the aggregation-vector spaces, and their l^p-coordinate models, such that eleven statements about completions of finite-support vectors on rooted trees hold simultaneously. These comprise: (1) completion statements saying that the root-sum tree space for the sequence tree and for the joined tree, and the zero-root space for the joined tree, are complete, infinite-dimensional, with continuous coordinates extending the vector coordinates, continuous potential fields P and Q extending the finite-tree ones, norm equal to P+Q at the root (or both P and Q at the root in the zero-root case, where the root coordinate vanishes), and with norm-nonincreasing idempotent coordinate projections onto initial subtrees having finite-dimensional range, closed finite-codimensional tails and approximation of tail elements by vectors vanishing on the head, and that XZero and XJoined are reflexive; (2) a main statement giving the lower bound t^3/128 on the averaged modulus of XSigma and XJoined for 0<t<1, a cubic-type uniform convexity inequality (‖x+z‖+‖x-z‖)/2 ≥ ‖x‖+‖z‖^3/(8(2‖x‖+‖z‖)^2) for x supported on a head and z vanishing there, and that no equivalent norm on XSigma, XZero or XJoined has the AUC property (positive modulus at every positive t); (3) positivity of the averaged modulus of XSigma at every positive radius t; (4) a separation statement for XJoined: for each ε>0 there is η in (0,1), equal to min(1/2, logarithmicGamma(2, ε/16)) when ε≤2, such that if ‖x±z_n‖≤1 for all n and the z_n are pairwise at distance at least ε, then ‖x‖≤1-η; (5) properties of the variable-exponent l^2-sum of height-h tree spaces with exponents 1+1/h, namely completeness, reflexivity, separable dual, a root-sum functional ν (nonnegative, definite, subadditive, absolutely homogeneous) bounded above and below by explicit multiples of the l^p norm, dense finitely supported vectors, and finite-rank projections; (6) a recursive characterization of the l^p-model potentials by least pairs, with ν equal to the root P plus Q; (7) for every equivalent norm A on the variable space, the modulus at lower/upper vanishes; (8) the absence of any equivalent AUC norm there; (9) a sixth-power stability inequality and (10) a cubic stability inequality for admissible heads, with explicit constants; and (11) a weak-tail estimate: if x and a weakly null sequence y_j with ‖y_j‖≥ε, 0<ε≤1, satisfy ‖x±y_j‖≤1, then ‖x‖≤θ(ε)<1.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/RecursivePotentials.lean; bytes 37649..37687
-- 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_RecursivePotentials

namespace OAI

noncomputable section

universe uIndex uSpace uOther uDomain uTarget uFiber

open scoped BigOperators

namespace ComparatorModel

open scoped BigOperators

namespace RecursivePotentials

Formal statement
theorem main : MainClaim := by
  sorry

end RecursivePotentials
end ComparatorModel
end
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/RecursivePotentials.lean
Human review
  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me