Exact Two-Dimensional SU(2) Yang-Mills in Lean: Weyl Integration, Heat-Kernel Convolution, Migdal Invariance, and the Exact Simple-Loop Area Law

Strengths

• The analytic normalizations are consistent: d_n=n+1 and character convolution has the factor 1/d_n. The bound |chi_n| <= n+1 gives the summable majorant sum_n (n+1)^2 exp(-t n(n+2)/4) for every t>0, supporting the stated convergence and coefficient-extraction arguments.
• The three-spoke change of variables is concrete and algebraically correct. Substitution removes the root coordinate by conjugation invariance, and the two subsequent integrations produce K_{t1+t2+t3}(abc) with the claimed noncommutative ordering.
• The finite-star and rooted-tree coordinate maps have explicit inverses and the appropriate triangular Haar-invariant structure. The manuscript correctly distinguishes the global vertex-coordinate transformation from an original-edge gauge fixing.
• For the recursively defined evaluator, schedule independence follows from the semigroup identity and enumeration of every face exactly once. Dual cycles do not invalidate this reduced-model argument.
• The correction notice directly addresses the historical abstract's overbroad reading. It preserves the analytic and reduced results while assigning the stronger original-edge claim to a separate successor, which is not evidence reviewed here.
• The full source commit and endpoint inventory are substantially more useful for reproduction than an unversioned repository citation. The notice also explicitly distinguishes its PDF audit from a full Lean rerun.

Weaknesses

• The central machine-certification claims remain reported rather than independently verified. Full theorem types, definitions, audit output and actual toolchain pins are external to this packet. This inspection limitation is not evidence that the public artifacts are absent.
• The human-readable dependency map jumps from orbital averaging to translated orthogonality. Identify scalar character orthogonality or its derivation, and explicitly state the Weyl integration formula advertised in the title.
• The reduced evaluator is defined through convolution. Its schedule independence does not itself establish geometric disk realization, physical edge elimination or isotopy invariance. The correction acknowledges this distinction, but it substantially limits the result's physical scope.
• No inspected comparison establishes which formalized components are new relative to existing libraries or repositories. The manuscript appropriately makes priority conditional; its strongest novelty claims should remain similarly qualified.

Potential errors

• Section 6.1, Eq. (6), states an identity for arbitrary diagonally invariant complex F without regularity hypotheses. For a non-Haar-measurable set A, F(x,y)=1_A(x^{-1}y) is invariant but has no ordinary Haar integral. State the Lean hypotheses or totalized-integral convention. This is a printed-statement ambiguity, not a counterexample to the Lean endpoint; continuous heat-kernel applications are unaffected.
• Section 7 identifies unit mass, but the displayed dependency map does not identify a theorem establishing K_t >= 0. Normalization alone does not justify probability terminology. Identify the positivity result or distinguish a normalized integral from a formally constructed probability expectation. This concerns documented formal coverage, not evidence that this classical heat kernel is negative.
• The Casimir n(n+2)/4 fixes a time/Laplacian normalization. Calling t physical Area(C) also requires a convention absorbing the Yang–Mills coupling scale. State that convention; no factor error is apparent within the explicitly defined heat-kernel model.

Strong novelty candidates

• Conditional on source verification and prior-art comparison: a concrete Lean chain from transported SU(2) Haar measure and moment-based orbital integration through all-label translated convolution to the infinite heat-kernel semigroup and actual two-face integration.
• Conditional formalization novelty in reusable finite-product Haar coordinate equivalences, connected-graph schedule construction and schedule-independent reduced Wilson coefficients. These are not claims of new mathematical identities or of the successor's original-edge closure.

Unresolved material objections

None reported.