# Verification report This report is licensed under the Creative Commons Attribution 4.0 International License (CC BY 4.0). **Problem:** AIM-PROBABILITY-0111 **Manuscript:** Nonuniformity of Free-Gradient Heat Semigroups under Finite Fisher Information **Report date:** 5 September 2026 **Review type:** internal, independent AI-agent mathematical and source audits ## Result and exact scope The audited argument gives a complete negative answer to the specified uniform-convergence question in the standard bounded self-adjoint tracial setting. It applies to every nonempty finite generating tuple $X_1,\ldots,X_m$, including $m=1$ and $m=2$, with finite **joint** nonmicrostates free Fisher information. The operator is the nonnegative self-adjoint generator obtained from the closure of the common polynomial column of free difference quotients, not a different deformation or a marginal compression. For each tuple the proof produces a constant $b>0$, independent of $t$, such that for every $t>0$ both the heat and resolvent defects on the operator-norm unit ball, measured in $L^2$, are at least $b$. Thus neither family converges uniformly to the identity as $t$ decreases to zero. The statement does not require compact resolvent, bounded or second conjugate variables, a nonamenability set, or $m\ge3$. The original source is the [AIM Free Analysis problem list](https://aimath.org/WWN/freeanalysis/freeanalysis.pdf), dated 24 August 2006, printed page 3, Section 0.3. The section is attributed to Dykema and Ricard; no individual proposer is attached to this paragraph. The related question on page 7 explicitly specifies the $L^2$ norm on the von Neumann algebra unit ball. Self-adjointness, the tracial probability normalization, and the closed-form realization are stated standard conventions, not additional restrictions printed verbatim in the target. Non-hyperfiniteness appears only in the source's subsequent rigidity consequence and is not imposed on the main theorem. ## Completed and pending gates | Gate | State | Evidence and boundary | |---|---|---| | Exact original problem and surrounding context | PASS | All seven source pages were inspected; the target and explicit norm paragraph were checked again during final review. | | All-variable source alignment | PASS | Nonempty finite tuples, including one and two variables; no stronger regularity or nonamenability premise was introduced. | | Marginal density implication | PASS | Conditional expectation gives the marginal conjugate variable; the Poisson/Cauchy-transform proof yields an actual $L^3$ density without assuming one. | | Generator-domain argument | PASS | Common-core approximation, the polynomial tensor adjoint formula, and graph-norm integration place the exponential witnesses in the full generator domain. | | Exact generator formula | PASS | Both contraction signs and their factor 2 were checked; the joint conjugate variable is never commuted with the coordinate. | | Real-line Fourier estimate | PASS | Independent derivation of the half-line projection/Fejer identity, its normalization, and the weighted $L^2$ consequence. | | Energy asymptotic | PASS | Duhamel/coarse-inner-product and approximate-identity calculations agree on the constant $2\pi\|\rho\|_2^2$. | | Fixed-time nonuniformity | PASS | Adjoint/resolvent duality and an independent spectral-moment argument give the same positive, time-independent defect bound. | | Assembled analytic proof | PASS | The complete dossier manuscript was independently read, including the final source alignment and limiting quantifiers. | | Attribution and bounded prior-art search | COMPLETED, LIMITED | Classical ingredients and relevant published hypotheses were checked. No matching all-variable theorem or complete argument was recovered in the bounded search; absence and priority are not certified. | | Transfer of audited proof into final LaTeX | PASS | The entire final source was read against the analytic proof; all hypotheses, domain steps, constants, both contraction signs and the qualified rigidity corollary are present. | | LaTeX compilation and bibliography/reference checks | PASS | Tectonic0.17.0 and BibTeX0.99d completed successfully. The final logs have no undefined references/citations, overfull/underfull boxes or missing-glyph diagnostics. | | Final PDF visual inspection | PASS | All11 pages were rendered at125dpi and personally inspected; all mathematics, citations and page boundaries are readable and unclipped. After adding two source URLs, pages1-10 were hash-identical and page11 was inspected again. | | Formal proof-assistant verification | NOT PERFORMED | No Lean, Isabelle, Coq, or other formal checker was used. | | External human peer review | NOT PERFORMED | Internal AI-agent reviews are not independent human refereeing. | | Numerical or symbolic-computer evidence as proof | NOT USED | All proofs and estimates are analytic. No finite computation substitutes for a quantified theorem. | These checks were completed on5 September2026. The final PDF has11 letter pages and the correct author metadata. The build and visual records are separate from the mathematical proof checks. A successful compilation does not constitute mathematical or human peer review. The first build failed while fetching the missing standard font cmmi5.pfb under restricted network access; an authorized network-enabled retry fetched the font and succeeded. A final ordinary build then also succeeded from the populated cache. The attempted bundled pdftotext path was unavailable; pypdf instead verified all11 text-bearing pages and PDF metadata. Neither environment issue was a LaTeX or mathematical failure. ## Attempted counterchecks The independent reviews specifically tried the following failure points: 1. **Narrowing the original problem.** The proof does not discard $m=1$ or $m=2$, add a non-hyperfiniteness premise, or replace the joint hypothesis by separate marginal assumptions. 2. **Degenerate tuples.** The empty tuple is outside the nonempty-tuple convention. Scalar or atomic coordinates are incompatible with the finite conjugate-variable hypothesis; they are not counterexamples. 3. **Only a form-domain calculation.** The exponential witnesses were placed in the operator domain before the adjoint pairings and second spectral moments were used. Polynomial tensors lie in the adjoint domain and are dense in the coarse Hilbert space; no unproved adjoint graph-core property is asserted. 4. **Unjustified commutation or invariance.** The joint conjugate variable need not commute with the chosen coordinate, and the full resolvent need not preserve its scalar subalgebra. Neither property is used. 5. **Circular density reasoning.** The Cauchy-transform argument starts with an arbitrary compactly supported marginal measure and derives its density by weak compactness; it does not assume absolute continuity or a pointwise Hilbert-transform characterization. 6. **Fourier normalization and the zero mode.** The negative half-line projection matches the declared Fourier sign. On the real line the singleton frequency zero contributes no additional mode. 7. **Weighted versus unweighted norms.** The Riesz projection is bounded on ordinary $L^3(dx)$. Holder's inequality then gives the required $L^2(\rho\,dx)$ bound with its density factor. No weighted-transform theorem or endpoint $L^\infty$ bound is assumed. 8. **Unbounded energy alone.** The proof also establishes an $O(s)$ bound on the generator of the oscillatory witness. The separate abstract example of an unbounded derivation with uniform heat convergence therefore does not contradict this argument. 9. **Interchanged limits.** The oscillation tends to infinity for each fixed heat/resolvent time. The resulting positive bound is independent of that time, so it excludes uniform convergence as time tends to zero. 10. **Complex versus self-adjoint unit balls.** Complex unitaries are legitimate witnesses. Splitting into their real and imaginary parts also produces self-adjoint contraction witnesses, with only a fixed loss in the lower bound. 11. **Unsupported rigidity corollaries.** The theorem concerns the exact semigroup. The source's rigidity consequence requires its named existing framework; no claim excluding arbitrary rigid subalgebras without the necessary normalizer hypotheses is inferred. ## Audit trail and provenance The repository's research dossier is `problems/AIM-PROBABILITY-0111/`. The completed evidence is recorded in: - `candidate_proof.md`: the consolidated analytic argument. - `source_recovery_agent.md` and `source_audit.md`: original source, conventions, adjoint-domain clarification, and source integrity. - `independent_proof_audit.md`, Section 10: the complete independent operator argument and its earlier unsuccessful or scoped routes. - `Fourier_estimate_audit.md`: independently derived harmonic estimates and the conditional resolvent lemma. - `final_full_scope_audit.md`: full source alignment and assembled-proof review, including the inspected-version record. - `literature_agent_audit.md` and `density_and_fourier_source_audit.md`: exact primary-theorem hypotheses, attribution, and bounded search limits. Earlier notes describing an unrestricted two-variable gap are retained as development history. The later all-variable argument supersedes that gap; the earlier notes are not represented as its proof. The one-variable density theorem, adjoint formula, Hilbert-transform boundedness, Plancherel theorem, and general semigroup tools are established mathematics. The density converse is attributed in Mingo--Speicher, Proposition 8.18, to Belinschi and Bercovici; the manuscript must not claim it as a new theorem. The candidate contribution is the application of these ingredients to the specified full-gradient nonuniformity question. The bounded literature search is not an absolute novelty guarantee. Third-party source PDFs remain research references in the dossier. This report does not grant a redistribution license, duplicate them into the paper package, or claim that their rights follow from an unrelated website license. The completed audits are internal AI-assisted checks, not human peer review or formal verification.