# Verification report — AMR-067-0008 (Gil-Medrano's problem on Berger projective spaces)

Verification date: 2026-10-09.

**Verdict.** The note is a partial answer to the second question of the record. In the Berger projective space
(RP^(2n+1), g_μ) it proves, in three regimes, that the projective subspaces RP(V) of one explicit type have the
least g_μ-volume among all competitors of their dimension, with the exact value of the minimum:
(I) projective hyperplanes, for every n ≥ 1 and every μ > 0;
(II) dimension 2j and type C^j ⊕ R, for 0 < μ < 1 and every n ≥ j ≥ 1;
(III) dimension 3 and type C ⊕ R^2 in RP^5, for every μ > 1.
The competitors are the countably rectifiable Borel sets that meet almost every complementary projective subspace.
They include the compact embedded C^1 submanifolds without boundary in the non-zero class mod 2 and the sets of
odd multiplicity of Lipschitz singular cycles mod 2. Among compact embedded C^1 submanifolds without boundary of
the non-zero class, the minimisers are exactly these projective subspaces. The regime μ > 1, n < k < 2n, n ≥ 3
remains open. The first question of the record was answered by G. Wheeler (arXiv:2607.24001), not by this note.
The note is unrefereed.

## Statement checked
- **Primary source.** F. Morgan and P. Pansu, "A list of open problems in differential geometry", São Paulo J.
  Math. Sci. 15 (2021) 305–321, doi:10.1007/s40863-019-00141-8, section "Area minimizing projective spaces in the
  projective space with the Berger metric", proposed by O. Gil-Medrano.
  - The section was read in the TeX source on the web page of P. Pansu.
  - For 2n + 1 > 3 and 0 < k < 2n + 1 it asks: (Q1) are the projective subspaces obtained from the k-dimensional
    equatorial spheres minimal submanifolds of (RP^(2n+1), g_μ)? (Q2) "Are they the only k-dimensional volume
    minimizing cycle in their homology classes?"
  - The source names no coefficient group. The note takes homology with coefficients Z_2: H_k(RP^(2n+1); Z_2) = Z_2,
    and for even k the RP(V) are not orientable.
- **Corpus record.** ulamai/UnsolvedMath, AMR-067-0008 (status `partially_solved`).
- **Wheeler's preprint.** G. Wheeler, "Minimal equators and homological systoles in Berger projective spaces",
  arXiv:2607.24001, version 1 of 27 July 2026; unrefereed; the only version on 9 October 2026 (arXiv API,
  00:18 UTC). It was read completely. Its N is n + 1. The note quotes its Theorems 1.1, 4.1, 5.3, 6.3, 6.4,
  Corollaries 4.2, 6.5, Propositions 4.3, 5.1, 5.6, Lemma 6.1, Definition 6.2, Conjecture 7.1 and Section 7. The
  quotations and their numbers were compared with the TeX source again in the fifth verification run.

## Readings
| Reading | Status | Where |
|---|---|---|
| Q1: are all RP(V) minimal? | answered by Wheeler: RP(V) is minimal exactly when V is of type C^c ⊕ R^r; not a result of this note | (W1) in Section 1.2 |
| Q2, literally: is every RP(V) volume minimising in its class? | no for μ ≠ 1 and 1 ≤ k ≤ 2n − 1: all RP(V) of one dimension are homologous and their volumes differ (Wheeler's comparison among linear subspaces) | Section 1.2 |
| Q2 as Wheeler's Conjecture 7.1: the distinguished type minimises among all cycles, and nothing else does | proved in the regimes I, II, III for the competitors of Definition 1.1 and for Lipschitz cycles mod 2; uniqueness among closed C^1 submanifolds of the non-zero class | Theorems I, II, III; Corollary 1.2 |
| the same for arbitrary flat chains mod 2 (the homological systole) | a remark that relies on cited theorems of geometric measure theory; not claimed as a theorem. For hypersurfaces: a self-contained proof in the class of sets of finite perimeter | Remark 3.9; Proposition 4.4, Remark 4.5 |
| uniqueness among all mass minimisers | a sketch only. For hypersurfaces: equality in Proposition 4.4 only for half-spheres | Remark 3.10; Proposition 4.4 |
| μ > 1, n < k < 2n, n ≥ 3 (first cases k = 4, 5 in RP^7) | open; a numerical probe only, labelled as not proved | Section 7.4; Problem 7.3 |

## Results in the paper
Notation: v_k is the volume of the round RP^k, M_j(μ) = 2F1(−1/2, j; j + 1/2; 1 − μ), m(μ) = (2/3)(μ^(3/2) − 1)/(μ − 1),
κ(W) is the cosine of the Kähler angle of a real 2-plane W, ν is the invariant probability measure on the
Grassmannian of real subspaces of codimension k.
- **Theorem I** (Theorem 4.2). For every countably 2n-rectifiable Borel set N in S^(2n+1),
  Vol_μ(N) = (μ vol(S^(2n))/2) ∫ (1 + (μ − 1)κ(W)^2)^(−(n+1)) #(N ∩ W) dν(W), the integral over the real 2-planes W.
  Hence every 2n-dimensional competitor has volume at least v_(2n) M_n(μ), the volume of a projective hyperplane, and
  a closed C^1 hypersurface of the non-zero class with this volume is a projective hyperplane.
- **Proposition 4.4.** A measurable subset E of the sphere with χ_E(−x) = 1 − χ_E(x) has g_μ-perimeter at least
  2 v_(2n) M_n(μ), with equality only for half-spheres.
- **Theorem II** (Theorem 5.1). For 0 ≤ b < 1 the common kernel W of j independent pairs (a, bJa + sqrt(1 − b^2) a')
  of Gaussian functionals satisfies E #(N ∩ W) = (2/vol(S^(2j))) ∫_N Φ_b(T_pN), with an explicit density Φ_b
  (Proposition 5.6: coefficients (2r − 1)!!(2j − 2r − 1)!!). An explicit positive measure on [0, sqrt(1 − μ)] of total
  mass M_j(μ) mixes the Φ_b to a function that is at most the Berger volume density, with equality exactly on the
  tangent planes of the spheres of type C^j ⊕ R. Hence the minimum v_(2j) M_j(μ) and the uniqueness statement.
- **Theorem III** (Theorem 6.1). In S^5, for μ > 1, the measure φ_μ(z_W) dν(W) on 3-dimensional subspaces, with an
  explicit positive rational function φ_μ of q = sqrt(1 + (μ − 1) z_W), has a Crofton density that is at most the Berger
  volume density, with equality exactly on the tangent planes of the spheres of type C ⊕ R^2. Hence the minimum
  v_3 m(μ) and the uniqueness statement. The measure is a mixture of the analytic continuations to negative
  t = b^2 of the Gaussian model "one correlated pair and one independent functional".
- **Corollary 1.2 / Proposition 3.8.** The set of points covered an odd number of times by a Lipschitz singular
  cycle mod 2 of the non-zero class is a competitor.
- **Proposition 6.9.** For μ > 1 no positive mixture of the invariant Gaussian models works in the case of
  Theorem III. **Remark 6.10** proves the reversed domination for 0 ≤ t < 1.
- **Proposition 7.1.** An exact weighted Crofton formula for every dimension k, with the weight
  (1 + (μ − 1)|K_W p|^2)^(−(n+1)) at the points p of the slice.
- **Tools.** Lemma 3.1 (law of row spaces), Lemma 3.2 (area formula for linear slices, Kac–Rice formula (1)),
  Lemma 3.4 (weighted Crofton formula for the invariant measure), Proposition 3.5 (the principle), Lemma 3.7
  (a compact submanifold met at most once by almost every complementary flat is a projective subspace).
- **Consequences, with Wheeler's theorems.** The least volume and the minimisers are determined for 0 < μ < 1 in
  every dimension and for every k, and in RP^5 for every k and μ; for μ > 1 they are determined for k ≤ n (Wheeler),
  k = 2n (Theorem I) and (n, k) = (2, 3) (Theorem III). The sense of "determined" is the one of the table of
  readings.

## Computations (scripts and outputs in reproducibility/)
No proof depends on a computation, and none depends on floating-point arithmetic: the identities used in the
proofs (Lemma 5.10, the derivatives in Lemmas 5.11 and 6.7, the integrals I_l and K_l, the closed form and the
positivity of φ_μ in Lemma 6.8) are proved in the text. The programs found the statements and test them.
- **Manuscript checks** (`manuscript_checks/`): 27 tests of the formulas as printed (exact, symbolic, 25 digits,
  one Monte Carlo test, one test on random planes in floating point); all pass.
- **Programs of the working stage** (`working_stage_theorem_I_and_surfaces/`, `working_stage_theorems_II_III/`):
  - exact and high-precision identities (`e1`, `e7`, `e11 M`, `e12`);
  - Monte Carlo tests of the densities (`e2`, `e9`, `e10`, `e11 G / K`; kernel of 2.4·10^9 slices);
  - both sides of the Crofton formulas on non-linear submanifolds (`verify_crofton*`, `verify_theoremD`, `e5`,
    `e13 X`). `verify_crofton_generic.py` was run twice: with 4·10^6 great circles two of the ten comparisons
    deviate by 2.8 and 2.2 standard errors (both in S^5; the other eight are within 1.8); with another seed, another
    hypersurface and 2·10^7 great circles all ten are within 1.3 standard errors. Both outputs are in the package,
    and the paper reports both;
  - the pointwise inequalities on random planes, on grids and by numerical minimisation (`e3`, `e15`);
  - searches for competitors of smaller volume (`verify_perturbation`, `e6`, `e13 V`): none found where the theorems
    apply, and found at once in control runs with the wrong sign of μ − 1;
  - the linear programme that led to Theorem III and the probe of the open cases (`e8`, `e8b`, `e14`);
  - checks of Wheeler's mean curvature and volume formulas (`verify_cone_exact`, `verify_first_variation`,
    `verify_sphere_numeric`, `verify_volumes`).
- **Rerun for this version** (`rerun_quick.py`, `reruns/`): the 16 quick programs were run again in a copy
  extracted from the archive `source.zip`; all end with exit code 0 and all checks pass. The outputs agree with
  the saved ones up to running times, one warning line and, for one program whose saved output had been produced
  with another seed, the random planes. The long Monte Carlo programs were not run again.
- **Programs of the five independent verification runs** (`independent_run_1_*` to `independent_run_5`), with
  their outputs.
- **Programs of the fifth run** (`independent_run_5/`, written from the formulas as printed, without the other
  programs):
  - `r5_exact_I_II.py`, 18 checks, exact or with 45 digits: Lemma 5.10 and the inversion of Proposition 5.6 for
    j ≤ 150; Lemma 5.11; the hypergeometric equation behind Remark 5.14(3) for j ≤ 150; the total masses; the
    constants of formula (7); all pass;
  - `r5_exact_III.py`, 31 checks: Lemma 6.5(b); the identity of Lemma 6.7 for 30 pairs (μ, x) (largest deviation
    3.5·10^−46); the closed form of φ_μ, derived symbolically from the base integral and compared with a
    quadrature of the defining integral for 48 pairs (μ, z) (largest relative deviation 1.1·10^−45); the positivity
    certificates; the total mass m(μ); Theorem 6.1(3) on a grid; all pass;
  - `r5_mc.py`: Monte Carlo tests of the Crofton densities of Theorem I, of Theorem II for j = 2 and of
    Theorem III, pointwise (from Lemma 3.2 alone) and end to end on small spheres that are not totally geodesic;
    4·10^6 samples per case; 115 comparisons, largest deviation 2.64 standard errors.

## Independent verification runs
Four independent verification runs, all AI-assisted, examined the working notes on 8 and 9 October 2026,
before the paper was written. Each run re-derived its part line by line, wrote its own programs and tried to
refute the statements. A fifth independent verification run, AI-assisted, examined the final text of the paper
on 9 October 2026.

| Run | Object | Verdict |
|---|---|---|
| 1 | Lemma 3.7; Theorem I (Crofton formula, inequality, equality case, value) | CONFIRMED; the summary statement about cycles: CONFIRMED_WITH_FIXES |
| 2 | the case j = 1 of Theorem II; cross-check of the mean curvature formula of Wheeler's preprint; the list of open cases | CONFIRMED (editorial fixes) |
| 3 | Theorem II for every j (all parts, including Lipschitz cycles); the remarks on hypersurfaces, on flat chains and on uniqueness | theorem CONFIRMED; remarks CONFIRMED_WITH_FIXES |
| 4 | Theorem III; Proposition 7.1 | CONFIRMED; presentation CONFIRMED_WITH_FIXES (editorial) |
| 5 | the final text: every statement and proof, first the parts written at the manuscript stage; the quotations from the sources; the package | CONFIRMED; CONFIRMED_WITH_FIXES for one measurability step, wording and reporting |

No run found an error in a statement or in a proof; the fifth run required one measurability step to be made
explicit (below). Contributions of the runs that are part of the paper:
the argument with sets of finite perimeter on which Proposition 4.4 is based (run 1); Proposition 6.9 and the
proposal of the extension from surfaces to all even dimensions (run 2); the direct proof of the total mass
mentioned in Remark 5.14 (run 3); the proof of Remark 6.10 (run 4); parts (a), second half, and (d) of Lemma 3.1
(run 5).

All required fixes of runs 1 to 4 were applied:
1. "Without boundary" in Lemma 3.7 and in the uniqueness statements.
2. The theorems are stated for the classes of competitors that are proved. The statement for flat chains mod 2 is
   Remark 3.9, with the cited theorems named; Proposition 4.4 gives a complete proof for hypersurfaces.
3. Uniqueness among all mass minimisers is Remark 3.10, labelled as a sketch; it uses that points of density one
   are regular points and an elementary argument in place of the constancy theorem.
4. Theorem I is presented as an application of the classical Crofton mechanism with an explicit positive
   density; no novelty is claimed for the mechanism; the sources that could not be read are named.
5. Credits: the classical method (Berger, Fomenko, Lê), Wheeler's proposal of a weighted Crofton formula, Tasaki,
   Kang–Tasaki and Bernig–Fu for the complex endpoint, Stecconi and Edelman–Kostlan for Kac–Rice formulas, the two
   preprints of September 2026 on RP^3.
6. Remark 5.13: the function ϱ_b is the density of the law of the kernel plane with respect to ν; its
   identification uses the injectivity of the cosine transform (cited), the exact Crofton formula does not.
7. Citations in Remark 3.9: Simon's lectures 17.6–17.8, Remark 17.9(1), Theorem 3.2(1); the paragraph numbers of
   Federer's book are marked as not checked.
8. Editorial additions in the proofs: charts and frames in Lemma 3.2; symmetric functions that are affine in each
   variable (Lemma 5.5); the exceptional sets are unions of fibres, and dim W ≥ 2, in Proposition 3.8.
9. The aside after the domination lemma for t ≤ 0 was replaced by the proved inequality of Remark 6.10.
10. Clarifications in Lemmas 6.2, 6.5 and 6.6 (the angle g, the invariant measure on flags, the tangent great
    sphere, the branch of the square root); formula (13) is used for non-negative functions only; one letter for
    one object.

Where the notes and the runs differed, the more careful version was taken:
- paragraph of Federer's book for homology of flat chains mod 2 (notes: 4.4.4; run 3: probably 4.4.6): the paper
  cites Section 4.4 and says that the numbers were not checked;
- regularity of minimisers mod 2 (notes: singular set of codimension at least 7 for hypersurfaces; run 3:
  codimension 2 in general, both attributed to Federer 1970): the paper uses neither;
- date of the preprint of G. Martins (run 2: 17 September 2026; notes: version 2 of 25 September 2026): the arXiv
  API gives version 1 on 17 and version 2 on 25 September; the paper cites version 2;
- novelty of Theorem I (notes: not found in the literature; run 1: an easy corollary of known theory, not found
  stated): the paper claims no novelty for the mechanism.

### The fifth run, on the final text
**Parts written at the manuscript stage**, which runs 1 to 4 had not seen: the common framework of Lemmas 3.1
and 3.4 and Proposition 3.5; the derivation of the formula of Theorem 4.2(a) from Lemma 3.4 instead of Santaló's
formula; Lemma 4.3 and Proposition 4.4 in their present form, including the equality case; the converse
statement in Lemma 5.8(ii); the derivation of the closed form of φ_μ in the proof of Lemma 6.8, which replaces a
simplification by computer algebra. The fifth run examined these parts first and confirmed all of them. It
re-derived the closed form of φ_μ step by step and symbolically, and confirmed it by quadrature with 45 digits.

**What the fifth run did.** It read the whole text and re-derived the proofs line by line (Sections 2 to 7); it
compared the question with the TeX source of the list, the quotations from Wheeler's preprint with its TeX
source, and the statements cited from Gil-Medrano (2016), Ambrozio's survey, Ambrozio–Marques–Neves,
Álvarez-Paiva–Berck, Torralbo–Urbano, Bernig–Fu, Simon's lectures and Hatcher's book with these sources; it
verified all 26 DOIs of the bibliography at Crossref and the three cited preprints at arXiv; it wrote the
programs of `independent_run_5/`; it extracted `source.zip` and ran `rerun_quick.py` there; it compared the
numbers quoted in Section 8 of the paper with the saved outputs; it repeated the literature search (arXiv,
OpenAlex, zbMATH, one web search; 9 October 2026, 00:18 to 00:28 UTC); and it looked at every page of the PDF.

**Result.** No error in a statement or in a proof. No proof depends on a computation. The quotations and their
numbers are correct. No new version of Wheeler's preprint and no other paper on the question was found.

**Fixes required by the fifth run, all applied:**
1. Lemma 3.1: the second half of part (a) and part (d), with their proofs. They make explicit a measurability
   step that Lemma 3.4, Proposition 3.5 and Proposition 3.8 use: sets of subspaces and functions of a subspace
   arise there as sets and functions of matrices, which are Lebesgue measurable but not known to be Borel.
2. Two sentences of the abstract. The sentence before the open case said that the second question is settled
   for 0 < μ < 1 and in RP^5; it now says that the least volume and the minimisers are determined in the classes
   of competitors named in the abstract. The sentence "we prove three further cases of the conjecture" now ends
   with "for the classes of competitors named below".
3. Three corrections in the description of the computations in Section 8: it reported only the second of the
   two runs of `verify_crofton_generic.py` and now reports both; `e1_exact_identities.py` checks the mixture
   identity for j ≤ 8 (not 10), with 25 to 40 digits; `e12_phi_closed_form.py` checks the integrals K_l by
   quadrature and the positivity of φ_μ by a certificate of its own, while the two certificates of the proof of
   Lemma 6.8 are checked by `manuscript_checks.py` and by the fifth run.
4. The Verification paragraph describes the final state, including this run; the sentence on the two papers that
   could not be read says what is the case (no openly accessible copy, no subscription; the publisher's page of
   one of them asks for a login); the theorem quoted from Álvarez-Paiva–Berck is stated there for integrands on R^n.
5. Wording and notation: the programs of the working stage are called so, in the paper and in the package
   (folders `working_stage_*`); a few sentences about program runs are in the passive voice; the case t = 0 of
   Remark 6.10; the letter for the element of O(m) in the proof of Lemma 3.1 and for the Killing tensor in
   Remark 4.7.

## Relation to the literature, novelty and scope
- **Searches (8 and 9 October 2026).** arXiv (Berger spheres and projective spaces with systoles, volume
  minimisation, Crofton formulas, Kähler angles; homological systoles; the name Gil-Medrano), OpenAlex (works
  citing the problem list, Gil-Medrano's note, Ambrozio–Marques–Neves, Álvarez-Paiva–Fernandes and Wheeler's
  preprint), zbMATH and the web; the verification runs made their own searches; the arXiv queries were repeated on
  8 October 2026 at 22:05 UTC, and the arXiv, OpenAlex and zbMATH queries and one web search in the fifth run on
  9 October 2026 at 00:20 UTC.
  - The only paper on the question that was found is Wheeler's preprint. It lists the three cases as open, and
    OpenAlex lists no work citing it.
  - No statement of Theorems I, II or III was found.
- **What is known.** The method is the classical integral-geometric proof of volume minimisation (Berger, Fomenko;
  Lê for homogeneous spaces; Howard's kinematic formula). The weighted Crofton formula for the unitary group is
  the first route proposed in Section 7 of Wheeler's preprint. For Theorem I: Crofton formulas for hypersurface
  integrands with extremal hyperplanes are due to Gelfand–Smirnov and Álvarez-Paiva–Fernandes (quoted from
  Álvarez-Paiva–Berck, last theorem of Section 5); according to Ambrozio's survey, Álvarez-Paiva and Fernandes
  classified the Finsler metrics on RP^n whose hyperplanes minimise the Holmes–Thompson area by positive measures
  on the space of lines. No novelty is claimed for this mechanism. The complex endpoint b = 1 of the family of
  Theorem II is Tasaki's Poincaré formula in the form of Bernig–Fu.
- **Not accessed.**
  - Gelfand–Smirnov (Adv. Math. 109, 1994) and Álvarez-Paiva–Fernandes (Selecta Math. 13, 2007): no openly
    accessible copy was found and there is no subscription (the publisher's page of the second paper asks for a
    login). It cannot be excluded that the inequality of Theorem I follows directly from a statement in these
    papers.
  - Tasaki (Math. Nachr. 252, 2003), Kang–Tasaki (Tsukuba J. Math. 25, 2001), Kang (Tokyo J. Math. 27, 2004): the
    publishers' sites refused automated access; what the note says about them is taken from Bernig–Fu
    (arXiv:0801.0711v9: Theorems 1.2, 3.9, 3.10, Corollary 5.14 were read) and from zbMATH reviews.
  - Federer's book, Fleming (1966), Allard (1972), and the works cited for attribution only (Berger 1972,
    Fomenko 1972, Borrelli–Gil-Medrano, Bray–Brendle–Eichmair–Neves, Lê, Howard, Santaló, Schneider,
    Edelman–Kostlan, Stecconi, Ambrozio–Montezuma) were not consulted. The statements quoted from Simon's lectures
    (open-access scan) and from Hatcher's book were read.
  - This negative search is not a proof of priority, and the note claims none.
- **Scope.** The note determines the minimisers in the regimes of its Table 1 within the classes of competitors
  named above. The statements about arbitrary flat chains mod 2 (Remarks 3.9, 3.10 and 4.5) rely on cited
  theorems and are not claimed as theorems. Remark 4.7 (metrics with minimal equators) relies on the cited theorem
  of Ambrozio, Marques and Neves. The proofs do not depend on Wheeler's preprint. Open: μ > 1, n < k < 2n, n ≥ 3;
  uniqueness among all mass-minimising flat cycles in Theorems II and III; a conceptual explanation of the
  measures.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/