Source and verification
This article explains family 072 of the October 6, 2026 OpenAI collection. The research conclusions are attributed to its manuscripts. The source review covers statements, introductions, and the proof mechanisms described below; it is not an independent verification of the complete proofs.
Overview
Family 072 studies how small or large the derivative of an injective holomorphic map can become near the boundary. One manuscript claims Brennan’s full integrability interval; its companion claims a strict improvement at inverse first powers, contradicting one value in Kraetzer’s proposed spectrum.
🏷️ Preliminaries: univalence and integral means
A holomorphic map is univalent if it is injective. Its derivative never vanishes. Let be the maps normalized by and , where is the unit disk. For real , define
Positive powers detect large derivatives; negative powers detect small derivatives. The integral-means exponent is
For the bounded-image subclass, write . The image bound is allowed to depend on the map. The supremum is taken after the limiting exponent for each map; a bound uniform over all maps is stronger information than this definition alone provides.
🏷️ Brennan’s formulation and the inverse map
Let be a conformal bijection and . Since and the area Jacobian is , change of variables gives
Consequently the interval becomes for . This calculation also explains why the domain need not be bounded: the problem can always be expressed on the disk.
Claims of the two manuscripts
For every , uniformly over and ,
The first manuscript claims and Brennan’s interval . The companion claims constants and such that
hence . (OpenAI, 2026) (OpenAI, 2026a)
The positive gap is existential, not a stated numerical improvement. The claim at does not establish a corresponding assertion at .
🏷️ A complete deduction for negative area powers
Suppose the inverse-square estimate holds. For , put . Jensen’s inequality for the concave function , with normalized angular measure, gives
Choose so that . Polar integration then shows that is area-integrable near the boundary. On compact subsets it is bounded, because is continuous and nonzero. This proves the negative-exponent portion of the area statement from the claimed radial estimate. The positive-exponent portion requires a separate argument; it does not follow from this interpolation.
The Koebe function illustrates the endpoint mechanisms. Its derivative is . Near , the inverse square behaves like , whose area integral diverges logarithmically. Near , behaves like , producing the opposite boundary exponent .
🏷️ The manuscript’s geometric contradiction
The source works on normalized maps of the upper half-plane. Recentring at transforms into
A positive operator averages such changes of base point, weighted by inverse derivatives. Hypothetical excessive integral-means growth produces a probability law with an exact scaling identity. Differentiation of that identity determines moments of the logarithmic derivative.
The second ingredient is a target-dependent potential, . Its critical points are organized into maxima and saddles. After proving that relevant superlevel sets cannot escape and that the pairing is measurable, the manuscript pairs each saddle with a maximum of at least the same potential value. An area formula converts this ordering into a sign constraint on an expected Jacobian. The weighted-law moments give the incompatible sign.
The inverse-first-power companion must also exclude equality. A merely nonpositive-versus-nonnegative comparison would give only . Its additional equality analysis is therefore essential to the claimed counterexample to Kraetzer’s prediction.
🏷️ Key steps and proof outlines
Growth creates an invariant weighted experiment
The contradiction starts with a positive operator on continuous functions of the compact normalized half-plane family. Its powers encode weighted derivative samples over successively finer dyadic scales. Let denote its spectral radius. If , define the positive resolvent and its maximum by
The identity gives
Iterating and using positivity yields , so . The resolvent therefore becomes unbounded at the spectral radius. Normalizing its evaluation at a maximizing map and passing to a weak limit produces an eigenmeasure. Averaging this measure over one horizontal period and one logarithmic scale interval gives the weighted affine law used in the proof. This is how a worst-case growth rate becomes a probability distribution on maps, rather than a choice of unrelated near-extremizers at every scale. (OpenAI, 2026b)
Escape estimates make the critical-point count legitimate
For a target , the potential need not have compact level sets merely because is univalent. A maximum or saddle could disappear through infinity or the real boundary. The source first derives weighted area integrability by applying the affine law to an inverse power of . The change of variables
has absolute real Jacobian . Combining this exact power with the scaling law converts integrability in one part of the half-plane into the boundary-weighted estimate needed elsewhere. Injectivity enters through the area formula: becomes ordinary area in the image, where inverse powers are integrable away from the normalized zero.
The escape lemmas then show compactness of relevant superlevels for almost every target. Only after this step can Morse-type counting compare saddles and maxima. Otherwise an apparent excess of saddles could be compensated by topology entering from the boundary.
Critical-point geometry becomes a Jacobian sign
The critical-point equation for can be solved for the target, giving a map whose preimages are critical points. Differentiating expresses its real Jacobian in terms of the pre-Schwarzian and the height . The weighted-law identities determine the moments of this logarithmic derivative, and therefore the expectation of the normalized Jacobian.
Independently, the superlevel count pairs saddles with maxima whose potential is at least as large. Apply the area formula separately on the positive and negative Jacobian loci of . This changes integration over source critical points into integration over target values with multiplicity. The pairing compares the two multiplicities with the appropriate weights. The resulting sign conflicts with the moment calculation if the putative derivative-growth exponent is too large. The measurable choice of pairing and the weighted treatment of exceptional targets are necessary to interchange this geometric argument with expectation.
Why the companion gives a strict improvement
The inverse-first-power argument has to rule out the borderline case where the Jacobian comparison is an equality. Its equality condition forces the pre-Schwarzian to be nonzero and satisfy . Consequently
is harmonic. On the rectangle , compare with a harmonic function that is zero, apart from the constant , on the sides and top, and has bottom values proportional to . Separation of variables gives the factor . At the fixed interior point , this factor is positive. The minimum principle would therefore force as , a contradiction.
Compactness then turns exclusion of equality into a uniform positive gap. The proof thus has two logically distinct conclusions: the transport comparison supplies a weak bound, and the harmonic barrier removes its equality case. The subsequent interpolation and area change of variables are the deductions described earlier, not substitutes for these two geometric arguments. (OpenAI, 2026a)
See Also
- Family 071: circle domains uses conformally invariant energy and boundary traces to control limiting conformal models.
- Family 080: Schrödinger endpoint convergence provides a different example where an arbitrarily small power loss must be distinguished from an exact endpoint estimate.
🏷️ Manuscripts and verification scope
- Brennan’s conjecture and sharp inverse-square integral means — the pinned manuscript; its directory supplies the source and citation metadata.
- A strict inverse-first-power bound for univalent functions — the pinned manuscript; its directory supplies the source and citation metadata.
The repository provides a formalization-scope page. Its scope description lists Brennan’s interval, sharpness statements, and the strict inverse-first-power estimate. These are statements about the repository’s documentation: no Lean build, axiom audit, or comparator-equivalence check was performed for this article.
OpenAI collection gives the reading sequence and source policy; coverage register records which families have articles and which remain to be written.