Reviews and checks

With it in its evidence: verdicts.json

Mathematical support

Milnor, Periodic orbits, external rays and the Mandelbrot set, arXiv:math/9905169, Theorem 6.5, is the relevant uniformization theorem. I read its statement and proof and visually inspected printed page 29. It gives the inverse multiplier parametrization and its interior holomorphic injectivity, uniqueness of the zero-multiplier center, and disjointness of component interiors. Thus distinct exact-period centers identify distinct hyperbolic components, and no hyperbolicity or boundary-area conjecture is needed to obtain a lower bound from any finite selection of them.

For an injective analytic map phi(t)=c+sum a_k t^k, change of variables and orthogonality on circles give area(phi(D_r))=pi sum k |a_k|^2 r^(2k). Letting r increase to 1 proves the nonnegative series formula used here. Partial sums are therefore valid lower bounds, irrespective of the omitted tail.

The contraction certificate is appropriate: the complex square contains the Euclidean disk; an enclosure of |1-Y G'_n| on that square bounds the Lipschitz constant on the convex disk. The strict self-mapping inequality and L<1 then establish a unique root. Excluding roots of every proper divisor establishes exact period. Different periods cannot represent the same attracting component of a quadratic polynomial; for equal periods, the center is unique.

At the center, write s(c) for the periodic point continuing 0. Implicit differentiation of f_c^n(s(c))=s(c), whose derivative in s vanishes there, gives s'(c)=G'_n(c). Differentiating the multiplier product gives lambda'(c)=2^n G'n(c) product{1<=j<n} f_c^j(0), as stated. The inverse's first derivative is its reciprocal.

The higher-coefficient method is also justified, but the paper should give a short explicit formal-series argument. At the exact center, s(0)=0, and the derivative of F(z,t)=f_{c+t}^n(z) with respect to z vanishes at (0,0). Starting with z=0 gives an error of order t; each iteration increases its order by at least one. After K iterations, coefficients through degree K equal those of the fixed periodic-point branch. Operations with the parameter ball enclose the same operations at its contained exact center. Setting the multiplier's constant term to exact zero is justified by the root certificate, not merely by an interval containing zero.

The overlap filter is conservative. All retained squares of the same period are pairwise disjoint. Converting exact endpoints to outward-widened binary64 endpoints may drop a genuine component but cannot create a false separation. Conjugate centers have equal component areas; a square strictly above the axis and its reflection cannot hold the same center.

Dyadic area bounds are rounded downward and summed as integers. My separate sanity check parses all input rows and compares the declared dyadic sum to the claimed threshold with exact rational arithmetic. These checks confirm internal arithmetic consistency and data dimensions, not the validity of every individual certificate. The small final conversion to a JSON float does not control this claim: the exact rational sum exceeds the stated threshold by a clear margin.

Johansson, Arb: Efficient Arbitrary-Precision Midpoint-Radius Interval Arithmetic, arXiv:1611.02831, describes the real/complex ball arithmetic and power-series facilities used here. It supports the numerical enclosure approach; it does not formally certify this Python implementation or the compiled library. The bundle accurately acknowledges that trust assumption.

Prior work and significance

Jay Hill's original 1997 report gives 1.506303622 from 430809 components and describes finding centers and recursively attached components before evaluating their areas. The component-summation strategy is established; the present contribution is its certified implementation and improved finite sum.

Thorsten Foerstemann's 2017 report, printed pages 7 and 9, reports the lower value 1.50640 and upper value 1.53121. I visually inspected Table II on page 9. Its implementation uses double-precision distance estimates, with an acknowledged interior-estimation inaccuracy. The present stated lower bound exceeds that reported lower value, while changing the assurance to enclosure arithmetic.

Claude Heiland-Allen's Trustworthy Mandelbrot, Area section, reports proven bounds 1.416492462158203125 and 1.84781646728515625 from interval-based classification. The current result improves that inspected rigorous lower bound. It does not improve the cited upper bounds.

Geoffrey Irving's ray-render README reports a Lean-verified upper bound near 1.826454. This is a different direction and assurance level; the present numerical lower bound should not be described as formally verified.

Hsing's current estimation page reports an estimate near 1.5065918902 with statistical uncertainty and discloses corrected confidence-interval calculations. It is context for the remaining numerical gap, not a rigorous upper bound.

The inspected primary sources support the paper's qualified comparison against the lower bounds it found. My search did not uncover a prior equal or stronger rigorous lower bound, but it is not an exhaustive historical-priority determination. I rate both claims moderate: a stronger reproducible enclosure bound and reusable certifier are advances others studying this area could use. They do not settle the exact area, close its rigorous interval tightly, or introduce a new uniformization theorem.

Minor fixes and limitations

1. Add the explicit finite formal-series stabilization argument above, distinguishing it from generic numerical convergence of fixed-point iteration.
2. Include the prior-work sources linked in the paper in references.json with claim associations. That file currently lists only Milnor and Johansson, omitting sources central to the novelty and comparison discussion. The prose links still make them accessible.
3. Qualify the explanation connecting slow convergence to Hausdorff dimension 2. Dimension alone does not determine the area of a boundary, its neighborhood decay, or the component-sum convergence rate. The reported threshold experiment may motivate a heuristic; it is not a consequence of Shishikura's dimension theorem.
4. Fix the search.c introductory example to include the required fourth argument 512, as the paper already does. The supplied certified input makes this search-example typo ancillary to both claims.

All node integrity arrays are empty. The UTF-8 files had no flagged invisible/control characters. The compressed data parsed into the declared row count with valid periods and decimal coordinates. The materials specify the pinned arithmetic packages, and the search is correctly separated from the certification. Floating-point reference areas in the tests are useful diagnostics, not substitutes for the enclosures. The full collection was not re-certified during this domain review. No formally checked theorem or unconditional global historical priority is asserted by this review.

With it in its evidence: checks.json, verdicts.json

Potential failure points inspected in C2:

• Existence is proved by a disk contraction, not by small floating-point residuals. The square interval encloses the disk; a uniform derivative bound below one plus the strict displacement inequality maps the disk into itself. The preconditioner is an exact midpoint, so its approximate choice is harmless if the inequalities pass.
• Excluding roots of G_d for every proper divisor d of n suffices for exact critical period. Exclusions are made on an enclosing square, a stronger sufficient condition.
• The multiplier derivative formula includes the derivative of G_n and the nonzero orbit factors. At a superattracting center the implicit periodic point has parameter derivative G_n', yielding the stated factor 2^n.
• For the longer series, iterating the period map from zero fixes an additional coefficient each pass: the actual fixed point vanishes at the center, and the multiplier has order at least one in the parameter displacement. After K passes the error is O(t^(K+1)). Thus truncation to K before multiplier reversion is justified at the certified center, even though interval boxes also contain noncenters. Replacing the enclosed constant multiplier by exact zero uses the proved center, not an arbitrary residual deletion.
• Same-period enclosures are deduplicated conservatively. If two contain the same center they intersect, so the sweep removes one. Rejecting an intersecting box rather than retaining it cannot increase area. Different exact periods cannot name the same component. Reflections count only boxes strictly above the real axis, and the same overlap check includes both halves.
• Dyadic lower endpoints are rounded down by integer shifts; summation is exact. The supplied numerator/denominator exceed 1.50651 exactly, independently of the displayed float. The independent check reproduces the down-rounded decimal and count identity; all 617591 data rows have valid finite upper-half-plane coordinates and positive integer periods, with maximum 512. This checks internal consistency, not that all ball computations passed.

No concrete counterexample, missing factor, unjustified series coefficient, duplicated-area mechanism or contradictory result was found. The exact rational total is the authoritative numerical result. The separate reproduction stage remains necessary to validate the full run, dependencies and all successful certificates.

Limitations and recommended improvements

The statement that nothing relies on floating point is too broad literally: outward box conversion uses Python's Fraction-to-float conversion and math.nextafter. On the usual correctly rounded binary64 platform, one outward nextafter encloses a nearest conversion and is conservative, so this is not a demonstrated defect. Document that trust assumption, or use exact rational comparisons for overlap elimination. Display bounds as decimal strings or the existing exact rational to avoid implying that binary64 storage itself is directed rounding. The claimed strict threshold has ample margin for a last-bit display difference.

Pinning python-flint and supplying an environment helps repeatability; it does not remove FLINT/Arb, interpreter, platform and hardware from the trusted computing base. The tests provide useful heuristic checks but do not replace interval certificates. Search completeness is unnecessary for a lower bound. I did not establish a global best-ever bound from all literature, and do not give a novelty verdict on such a stronger statement.

Deterministic integrity flags

No missing sections, required files, unlisted identifier citations or data integrity findings were reported. The orphan 'ten' describes decimal display precision, not an unbound empirical observation; place this convention in Methods or bind it in the schema. Both allegedly uncited references are actually linked through ordinary source URLs in the prose. Use their arxiv:math/9905169 and doi:10.1109/TC.2017.2690633 identifiers consistently so the ledger resolves the citations. These are presentation/auditability recommendations, not refutations of C1 or C2.

Prior work checked

Milnor (1999), Theorem 6.5, was read directly in the primary arXiv PDF, as above. The standard theory is known; the contribution here is the finite certified sum and reproducible data/verifier, not a new uniformization theorem. Primary historical links cited by the paper were attempted (Hill/MROB, mathr, Foerstemann), but the retrieved pages did not yield the stated numeric comparisons in searchable text; I therefore do not certify the paper's comprehensive priority comparison. This limitation does not change the two bounded claims under review.

With it in its evidence: independent_checks.json, independent_checks.py