# AI provenance: Proving Conjectures of Ashoke Sen: F-Theory Limits, Small Black Holes and Dyon Indices

(Earlier title: Conjectures of Ashoke Sen: Scope, Exact Tests and Analytic Limits.)

Author:
- Deep Bhattacharjee, sole and corresponding author. ORCID 0000-0003-0466-750X; d.bhattacharjee@erl-forschung.de, itsdeep@live.com, egspl@proton.me (GitHub-related contact); GitHub creelie. Formerly Electro-Gravitational Space Propulsion Laboratory (EGSPL), Bhubaneswar, Odisha 751030, India; formerly University of Calcutta (Heramba Chandra College), 23/49 Gariahat Road, Golpark, Kolkata 700029, West Bengal, India.

- Paper and source: https://github.com/creelie/Paper_11, release v2.2.1, version DOI https://doi.org/10.5281/zenodo.23749469. The concept record https://doi.org/10.5281/zenodo.23652472 lists every version.

## Result

The paper examines thirty-six statements of Ashoke Sen and the two heuristic statements of his matrix theory paper. For each it gives the original hypotheses, what was derived, the later tests and proofs, and a verdict.

- **Claim 23 (weak coupling of F-theory).** Every degeneration of F-theory on an elliptic Calabi–Yau variety that is weakly coupled at the generic point of the base is, after a base change of degree 1 or 2 and a rescaling, Sen's family f = −3h² + tη, g = −2h³ + thη − t²χ/12. Such a degeneration exists exactly when −2K_B has a section. Rigid curves of self-intersection −n lie in the zero locus of h. On a surface whose anticanonical system has no base points, the D7 singularity of a general member is a set of nodes, with 2χ(Y) = 4χ(O) + χ(D̃); without that hypothesis it fails, as the Hirzebruch surface F12 shows.
- **Claim 26 (small black holes).** For every action whose corrections are built from curvature, the entropy of the two-charge horizon is 4π√(nw)·√(R*/α′), with R* one critical value. The Gauss–Bonnet truncation gives the statistical value exactly in D = 4 and 5, as Sen states. Prester's Lovelock completion gives it in every dimension with a unique solution, and its coefficients are the only ones that do.
- **The heterotic string in D ≥ 6 (in a highlighted box; not a claim of Sen).** Assume the central-charge route of Dabholkar–Murthy and Kraus–Larsen–Shah. Then Sen's value holds if and only if c_R = 12N. The nonlinear superconformal algebras with sixteen supercharges give a non-unitary theory (D = 7, 8), or c_R ≠ 12N (D = 8, 9, 10), or no algebra at all (D = 6). So the route does not give the value in any D ≥ 6. Whether the complete heterotic action gives it remains open.
- **Highlights.** The paper marks three kinds of statement:
  - rose: a statement Sen printed that is false as printed;
  - burnt orange: a statement that fails under its own hypotheses (fatal);
  - yellow: what is left unproved.

  No statement of Sen examined is wrong as printed or fatal. A table lists, claim by claim, what is left unproved.
- **Exact tests.**
  - Exact product expansions reproduce the negative full dyon indices of the toroidal orbifolds: thirty charge triples in the scanned cone.
  - Two misprints in the tables of Chattopadhyaya and David are corrected.
  - The tachyon-dust caustic is given its characteristic flow and the hypotheses under which it is attained.

## Who did what

Text of the contribution: a mix of human-written and AI-generated text.

Human understanding: all parts. The author read every proof and approved the final text.

Deep Bhattacharjee chose the problem and the claims, directed the work, set the format and ran the computations. The following were produced with AI assistance under his direction:
- the proofs and the text;
- the figures;
- the Lean files;
- the Python checks;
- the reference list.

The AI tools were Claude Opus 5.5 in Claude Code, Claude Fable 5.1 with Ultracode, GPT-6.1 Sol Ultra and GPT-6 Astra Ultra. Every quotation of Sen was compared with his arXiv source, and every reference was checked against the publisher's, Crossref's or arXiv's record.

## How the result is checked

- **Lean 4.** `lean/SenConjectures.lean` (Lean 4.34.1, no library) has fifty-seven theorems, each depending on no axiom or on `propext` alone. It recomputes the coefficient tables inside the kernel from the definitions of the theta functions, and checks the wall-crossing identities and the twenty-one negative triples with P² ≤ 4 and Q·P ≤ 2.
- **Exact arithmetic (Python).**
  - `code/siegel_dyons.py` computes every table.
  - `verify_revision.py` rechecks the thirty-triple scan.
  - `verify_infrared_estimates.py` checks the constants of Appendices E and F.
- **The closures.** `code/verify_closures.py` (sympy, mpmath) makes 346 checks of the identities and numbers of Appendix G for claims 23 and 26.
- **The central-charge theorem.** It is elementary algebra and is proved in full in the box. Its four central-charge formulas are those of Kraus–Larsen–Shah, Table 2.
- **Workflow.** The verify workflow reruns the Lean and Python checks on every push.

## What is not claimed

- The identification of the weak coupling limit with a type IIB orientifold beyond its geometry is not proved. The normal form is a statement about Weierstrass curves over K(B)((ε)), the Laurent series in the parameter over the function field of B; it does not by itself describe the total space of the family.
- The statements on the nodes of the D7 divisor are not claimed when the anticanonical system has base points.
- The statement that the complete heterotic effective action gives 4π√(nw) in every D ≥ 6 is not proved. The central-charge theorem settles that route under its stated hypotheses, and those hypotheses are themselves not proved.
- The confirmed and heuristic claims of the catalogue are not proved; the table of what is left unproved names the missing step of each.
- The proofs are written by hand and have not yet been refereed.