Exact rational certificates for real tangency counts: 144 tritangent circles, and a twelve-integer witness for circles tangent to a conic and two lines
Abstract
Three general conics in the plane admit 184 complex circles tangent to all three, and Breiding, Lindberg, Ong and Sommer conjectured that at most 136 of them can be real. Brysiewicz has recently refuted that conjecture by exhibiting a triple of conics with 144 real tritangent circles, certified numerically with interval arithmetic. We give a proof of his lower bound that uses no floating point and no interval library: an exact rational certificate, checked symbolically, for each of the 144 circles. The certificate format is elementary and reusable. Every equation of a marked tangency system has total degree two, so the divided difference F(x)-F(y)=J_F((x+y)/(2))(x-y) holds exactly; a Newton-like map is then a contraction on a box as soon as two rational inequalities hold, and the Banach fixed point theorem—rather than Brouwer or degree theory—produces the zero. We apply the same certificate to the constituent problem QL², circles tangent to one conic and two lines, whose maximal real count Fiorelli Vilmart posed as an open problem and whose current record of 14, out of 16 complex, is an ingredient of the count 144; his appendix certifies the nine-variable tritangent system and none of the four constituent problems, so that 14 carries no certificate. We certify 14 for his own limiting configuration, and exhibit a second configuration attaining 14 whose conic and two lines have twelve integer coefficients of at most three digits. We also record two octics whose roots are the QL² solutions on the two bisectors, the identity F₁+F₂=(1+m²)D² they satisfy, and the resulting localisation of the two families of eight in complementary double wedges. The counts 144 and 14 are Brysiewicz's; what is new here is the exact certification, the small witness, and the bisector structure. We do not prove that these counts are exact, and we do not settle whether 16 is attainable. Everything proved below is machine-checked in Lean 4 against Mathlib, except where the text says otherwise.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
cb4cc88cc911a84aaa0a8e64d4db48063ed3078b43a652f5c5556a64b919b1f3
Claim ledger
Stated results
TK1routine2026-09-03
Soundness of the rational contraction certificate for square systems of quadratics: the exact divided difference F(x)-F(y)=J((x+y)/2)(x-y), CHECK A and CHECK B give a real zero in the box
TT1known data2026-09-03
At least 144 real circles are tangent to the three conics of arXiv:2609.01521 eq. (1), each tangent at a real smooth point of each conic, each with positive squared radius, pairwise distinct as circles – so the maximal number of real tritangent circles is at least 144 > 136
TT2routine2026-09-03
Negative controls for the 144-witness certificate: a centre displaced by 2⁻30, a box radius of 2⁻4, and the midpoint of two certified centres are all rejected; the system is not the zero system
TQ1known data2026-09-03
The QL² limiting configuration of arXiv:2609.01521 (the conic 20u²-5v²+1 with the two axes L1, L2 of its degenerating conics) has at least 14 real tangent circles, tangency points real and smooth, squared radii positive, pairwise distinct as circles
TQ2candidate2026-09-03
A twelve-integer configuration – the conic -19u²-48uv+107v²-71u+32v+3 and the lines 24u+115v-58, 43u+108v+46 – has at least 14 real tangent circles, i.e. attains the QL² record with data three orders of magnitude smaller than the source's
TQ4routine2026-09-03
Negative controls for the paper's QL² certificate, including refusal of the real part of a non-real solution of the degree-16 eliminant
TQ5routine2026-09-03
Negative controls for the twelve-integer QL² certificate
TP1routine2026-09-03
The two-octic pencil identities for QL² in normalised position: F1+F2=(1+m²)D², F1=S*U+m²*D², F2=D²-S*U with S=a²+b², U=Y²-m²X², D=W(XY'-YX'), and the tangency identity a*Phi_X+b*Phi_Y=0 along a parametrised conic
TP2routine2026-09-03
Wedge localisation for QL²: F1 and F2 are never both negative, every real u-axis solution has U <= 0 and every real v-axis solution U >= 0, so a conic strictly inside one wedge contributes no solution on the other bisector
TP3routine2026-09-03
Reconstruction: a real root of the octic F1 at which the parametrisation is finite and the tangent is not vertical really is a real circle tangent to the conic and to both lines, with centre P/(Wa) on the bisector and squared radius m² s²/(1+m²)
TM1measurement2026-09-03
Census: 1411 independent exact hill climbs (4.23 million exact Sturm evaluations, 2.0 CPU-hours) in the normalised two-bisector parametrisation of QL² terminate at real counts 4, 6, 8, 10, 12 or 14 (12 in 1164 of them, 14 in 11) and never at 16
This ledger entry is reported in prose and is not bound to a Lean theorem.TM2measurement2026-09-03
Encoding measurement: 12 960 dyadic certificate entries written as rationals n/2⁸0 do not finish elaborating (killed at 30 minutes at maxHeartbeats 10⁶); written as integers with the scaling moved into one function they elaborate in 142 s, and the theorem module on top in 24 s
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- For three general complex conics in the plane there are exactly 184 circles tangent to all three (Breiding–Lindberg–Ong–Sommer, *Real circles tangent to 3 conics*, Le Matematiche 78 (2023) 149–175, arXiv:2211.06876). How many of the 184 can be real? BLOS conjectured the maximum is 136 (their Conjecture 1.4). Taylor Brysiewicz, *144 real circles tangent to three conics*, arXiv:2609.01521v1 (math.AG, 2026-09-01), disproves it by exhibiting a triple with 144.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7