# Preliminary audit—repair verification ongoing # Bader–Fisher–Miller–Stover: source-adjudicated progress report 21 October 2026. **Current scoped report; theorem-level review remains open.** The supplied proof has definite local defects. No counterexample to a headline theorem has been found in this campaign. We now have a written proposed completion of Lemma 3.5, including the exceptional parabolics in dimensions four and seven, with exact checks of their radical structures. This substantially advances the repair work, but does not establish the entire arithmeticity theorem independently. ## Scope and editions The native panel reviewed arXiv 1903.08467v5 (26 April 2020), using the received-date cutoff of 20 June 2019. The frozen Annals manuscript was compared separately where specified below. Journal-only wording is not attributed to a model that saw only the preprint. Later papers and supplied subscription-model reviews are separately attributed evidence, not admissible original-proof inputs by default. Sol returned a full-paper report and all sixteen local/prose assessments. Gemini returned two local assessments. All three Opus attempts exhausted their caps. Two Gemini arbitrations were rejected because their reference-to-finding evidence violated the chronology contract; they are preserved, not counted as accepted arbitral verdicts. The Astra and Fable texts supplied by the user both endorse the main result after repairs, but those endorsements are not this campaign's independent certification. ## Missing support condition Proposition 3.1(3) omits proper support. The constant sequence of normalized Haar measures satisfies the printed homogeneous/ergodic/convergence condition for any lattice: restriction to the noncompact subgroup W is ergodic by Howe–Moore. Consequently the printed condition has no arithmeticity content. Adding proper support changes that condition and is necessary; it must not be described as a proof of the original literal formulation. This does not invalidate the needed direction from infinitely many distinct maximal totally geodesic subspaces to properly supported approximating measures. That direction, including its nonescape and support-containment steps, needs its own source-based audit. The graph records the original statement defect separately from the main result. ## Lifting measures The journal's displayed orbit identity requires S_i=x_i⁻¹S′_ix_i and Γ_i=x_i⁻¹Γ′_ix_i=S_i∩Γ. The printed reversed conjugations were checked directly against the frozen journal pages. They are readily corrected algebraic errors in wording absent from the corresponding native-v5 passage. The exceptional n=3 argument also needs more than nonnormality of Γ_i and injectivity of ρ: those properties do not prevent an image from lying in one direct factor. The appropriate geometric argument uses the diagonal/subdirect complexified Fuchsian subgroup. Its descent and the faithful irreducible representation over the relevant local forms remain open checks in this campaign. The supplied replacement using the two adjoint modules is recorded as a proposal, not automatically accepted. ## Compatibility lemma The original proof of Lemma 3.5 omits the n=4,a=2 and n=7,a=4 parabolic possibilities. It also uses false auxiliary assertions: not every noncentral subgroup of P contains U; SO(4,C) is not almost simple; a parabolic's unipotent elements need not lie in its radical; and containing a derived Levi and the radical does not by itself supply the missing Levi torus. The new [proposed completion](compatibility-repair.md) addresses these points. The dimension of the image of U gives a full-rank constraint. Full Levi projection and normality put the two relevant normal unipotent groups into the radical; a dimension comparison then excludes the nonabelian Heisenberg case and retains the abelian triality case. The n=3 quotient case is treated separately. The note identifies all standard algebraic-group prerequisites and does not use the later complex-hyperbolic sequel as a proof input. The [exact checker](exact-check.py) verifies the exceptional radicals using rational matrices; [results](exact-results.json) include source and checker hashes. These computations check the local structures, not the general rank/Levi theorems or the main arithmeticity argument. Pending independent checking of the assembled replacement, the graph leaves the original local proof red, with its statement unresolved by the campaign rather than falsely marking it refuted. ## Superrigidity and external sources The short repair of A-initiality is checked: an initial A-object H/J_A maps equivariantly to the existing H-valued A-object. Freeness of left translation forces J_A=1, and an H-equivariant map H→H is a translation, hence an isomorphism. This fixes that local inference; it does not discharge the entire superrigidity proof. The retrieved 3 October 2018 Bader–Furman preprint, arXiv 1810.01607v1, supplies the applicable initial-object theorem (4.3), normalizer theorem (4.6), and gluing lemma (5.1). Their statements, hypotheses, and equivariance convention were checked; inversion converts the left/right conventions. The BFMS bibliography's arXiv number 1810.01608 is wrong. The proofs of the entire imported framework have not been reproduced. The normal-subgroup-chain passage from U′ through U to P still needs a complete written audit; an equality of iterated normalizers cannot simply be assumed. The distinct-place deduction, including the non-absolutely-simple n=3 case, also remains to be checked through all hypotheses. These outstanding obligations prevent an unconditional campaign-level green badge. ## Graph, cost, and next checks The decorated graph at the top of this panel page uses only explicitly source-audited proof dependencies. Its arrow relation is prerequisite → consumer. Red refers to the original local statement/proof described in the explanation; yellow can mean unadjudicated or blocked. The graph is a partial map, so its sinks are not a complete inventory of advertised results. All other extracted references remain in the original reading roadmap. All paid work is terminal: 24 attempts, 19 usable initial assessments, three capped/incomplete attempts, and two invalid arbitrations. Recorded usage-based cost ceiling is **$3.6275665** against $10 authorized, including failures; this is not invoice reconciliation. No new API calls or retries were made for this adjudication. Next mathematical work: independently scrutinize the proposed compatibility completion; finish lifting/descent, the normal-subgroup-chain argument, the distinct-place reduction, and essential dynamical reference hypotheses. No paper-level claim of correctness, falsity, or completed repair is inferred from model agreement. ## Reports and reproducibility [Independent model outputs and attempt coverage](panel-assessments.md) · [Coverage and costs](coverage-and-cost.md) · [Exact-check instructions](reproducibility.md). All native calls are terminal. Publication does not imply that the proposed corrections have been fully verified.