# Chaika–Forni: preliminary proof audit **Substantive defects in the supplied proof; main weak-mixing statements unresolved in this audit.** Jon Chaika and Giovanni Forni, *Weakly mixing polygonal billiards*, Annals of Mathematics **203** (2026), 695–735. The independent native reviews used arXiv 2003.00890v2 (14 August 2025). The supplied 41-page journal PDF was subsequently checked at the relevant locations. This is a preliminary audit, not a complete replacement proof or an independently certified refutation of a main theorem. ## What is established by the checks recorded here 1. **Theorem 1.3's proof does not justify its passage from a projected component back to the original lattice-distance claim.** On journal pp. 726–728 the proof projects the translated cohomology section to the positive-exponent part, derives a distance estimate for that projection, then concludes that the original class violates the eigenvalue condition. No integral-lattice compatibility or full-residual estimate is supplied at that passage. 2. **The final growth step in Proposition 5.1 loses a required hypothesis.** On journal p. 718, after (21), the proof applies the preceding growth argument to the original section minus a parallel integral section. The growth input requires membership in a specified positive-exponent invariant subbundle. Subtracting an arbitrary integral section does not preserve membership. 3. **The measure-loss estimate in the iteration has an unsupported inequality.** The sequence x_j is established as a lower bound for the actual distances in (34), journal p. 727. The following bound in (35), p. 728, charges exceptional measure using x_j to the positive power sigma. A bound on losses using the actual scale cannot be replaced by a bound using its lower bound without a further argument. The parameter-dependent continuation windows also need a measure/covering argument. 4. **A local uniqueness/transversality assertion in Lemma 6.2 is false.** The scalar equation in that proof can have two solutions and can have a double root. Exact square-torus examples and a checked weaker null-set replacement are given below. This local correction does not repair the §6 iteration. These findings are coordinating source checks, separately attributed from model assessments and automated arbitration. Source passages, scope and graph bindings are retained in `decision-records.json` and `proof-edge-audit.json`. ## Why projection and integral translation matter Let d_Z(v) denote distance to integral cohomology. For an arbitrary invariant projection P, neither P(H^1(Z)) contained in H^1(Z) nor preservation of d_Z follows from boundedness or equivariance. Already in Euclidean space, v=(1,0) is integral, but its orthogonal projection to the diagonal is (1/2,1/2), whose distance to Z^2 is sqrt(2)/2. This refutes the general implication needed by a projection argument; it is not a translation-surface counterexample to Theorem 1.3. An additional geometric argument could conceivably supply the missing comparison, but none has been verified here. Similarly, for a subbundle F and an integral section z, phi in F does not imply phi-z in F. The text on p. 718 applies the growth argument after this subtraction without establishing its bundle hypothesis. This is more than changing a constant. It does not by itself prove that Proposition 5.1 is false under its single strongly irreducible bundle hypothesis. ## The supplied cyclic-cover counterexample An external review attributed by the user to Astra supplies a detailed candidate on M10(1,1,1,7). The proposed identity is f_n-z_n=-e_n, with f_n in the positive-exponent part, z_n integral and e_n arbitrarily small in a Hodge-isometric part. If all the stated bundle and recurrence hypotheses hold, this gives d_Z(C(g)f_n) at most |e_n| for every transport, contradicting the growth demanded by Corollary 5.2 even with its intended range restriction. Our exact checks confirm the genus, zero orders, complete deck-character dimension table, the exponent 2/5 obtained from the cited EKZ formula, and the cyclotomic algebra producing the integral approximants. We have not completed our independent verification of the finite-cover/strong-irreducibility and recurrence/admissibility details. Consequently **this package does not mark Corollary 5.2 refuted under its intended positive-exponent hypotheses**. The full proposed construction, what has been checked and the remaining obligations are recorded separately. The published corollary also has a displayed range omission; the stronger candidate explicitly aims to survive correcting it. ## A checked local correction: Lemma 6.2 On the unit square torus with omega=dx+i dy, take alpha=3 and z=4[dy]. The displayed scalar equation with a=0 is 3 sqrt(1+s^2)=4. It has the two solutions s=+sqrt(7)/3 and s=-sqrt(7)/3, both in [-1,1]. With alpha=1 and z=[dy], the residual is (sqrt(1+s^2)-1)[dy], with a double zero at s=0. Thus uniqueness and literal transversality cannot hold universally as asserted. The weaker null-set conclusion has a short replacement. For fixed integral z, squaring alpha sqrt(1+s^2)=a s+b gives $$ (\alpha^2-a^2)s^2-2ab s+(\alpha^2-b^2)=0. $$ For nonzero alpha this polynomial cannot vanish identically: its coefficients would require a^2=b^2=alpha^2 and ab=0. Thus each z contributes at most two solutions. Integral cohomology is countable, so their union is null. This is a verified replacement for the weaker conclusion, not a proof of the false transversality assertion or of the main theorem. ## What remains disputed or unverified The final proof uses fixed-time recurrence estimates at parameter-dependent stopping times. This remains a precisely located obligation; the present audit has not supplied a stopping partition or established a counterexample to that particular recurrence assertion. There is a genuine native-model disagreement about Lemma 4.8. Sol flags endpoint, floor-counting and time-offset gaps; Gemini explains how some losses can be absorbed using slack and larger time thresholds. Neither agreement with Sol nor Gemini's proposed completion is treated as source adjudication. That lemma remains unresolved here. Sol also flags issues in the polygon phase-space identification and continuity argument. These are retained as model findings pending complete source checks. No full replacement for §§5–7 has been verified. Principal external inputs are not comprehensively theorem-audited. Historical publication years in the bibliography are not inspection of the corresponding theorem statements. ## Context of the main claim The introduction identifies the dense-G-delta weak-mixing conclusion as answering a conjecture of Gutkin and Katok, cited to their 1988 paper, §1. This attribution has been checked in the manuscript; the original 1988 conjecture text has not been independently compared here. Theorem 1.1 is the existence formulation; Theorems 1.2 and 1.3 are the proposed spectral route. Familiarity or plausibility of those conclusions cannot discharge a failed inference in this proof. ## Actual panel coverage and costs One complete-source Sol review and four of eight targeted reviews returned usable assessments: three targeted Sol reports and one Gemini report. The initial requests did not contain Astra's report or the supplied cyclic-cover example. The remaining targeted attempts were capped or failed validation. All three arbitration attempts failed to produce an accepted verdict. In two Gemini responses, background/retrospective reference records also carried finding links, which violates the strict annotation contract. That rejection alone does not establish mathematical reliance on a later theorem. Those responses remain excluded from accepted arbitration evidence. Opus exhausted its output cap. Total usage-based conservative accounting is **$3.9399455** against a $10 authorization, including failed attempts. This is API token accounting, not an invoice. There were no generation retries. No paid Astra or Fable calls were made in this campaign. Details are in the coverage record. The present conclusion is therefore scoped: the source checks establish substantive defects and a false local assertion. A main-theorem counterexample, a completed repair and the full intended-range corollary refutation are not established by this package.