Internal proof audit

Henry Zweiman. September 15, 2026. Conducted by the originating assistant; not independent review.

Main comparison

1. Operator normalization. A is nonnegative minus the second derivative. The heat semigroup is exp(-tA). The interval is Neumann at 0 and Dirichlet at L, matching decreasing rearrangement. Reflection aligns it with the primary source.
2. Graph hypotheses. Finite positive-length edges, nonempty Dirichlet set, and connectivity outside that set are explicit. Loops count twice in vertex sums. Dirichlet vertices need not be leaves for the inequality. Degree-two subdivisions do not change the problem.
3. Regular resolvent loads. Strictly positive nonconstant edgewise polynomials are dense in the nonnegative L2 cone and need no vertex compatibility. The resolvent is analytic past each closed edge. A constant solution edge would force a constant polynomial load, which is excluded. Thus critical values are finite in the approximation step. The proof does not incorrectly assume this for arbitrary L2 data.
4. Flux sign. Integration over a superlevel set gives h times the sum of absolute boundary derivatives, with a positive sign. Internal vertex fluxes cancel because every incidence near an included vertex belongs to the superlevel set. Positive levels contain no Dirichlet vertices.
5. One boundary point is sufficient. A simple path from a maximum to the zero Dirichlet set crosses every intermediate value. Hence N>=1 even with cycles or multiple edges. Cauchy-Schwarz gives ab>=N squared, and therefore -hU''+U<=F, in the needed direction.
6. No hidden singular part. The path-length estimate makes the rearrangement globally Lipschitz. The nonflat analytic approximation makes exceptional mass ranks finite. Thus U is W2-infinity and the differential inequality has a valid weak interpretation. Its mixed boundary data are U(0)=0 and U'(L)=0; the latter follows from essential infimum zero, not from giving a point positive measure.
7. Interval monotonicity. The resolvent derivative has nonpositive forcing and nonpositive endpoint data. Positive-part testing gives a decreasing interval profile. Monotone smooth approximation handles rough decreasing data.
8. Cumulative-order induction. The interval cumulative equation preserves concentration order. This is essential: a comparison only against the rearranged previous graph profile would not by itself justify iteration without that order property.
9. Density and Euler limit. Hardy-Littlewood proves L2 contraction of decreasing rearrangement. Resolvent boundedness passes the regular-load inequality to general loads. Spectral dominated convergence proves the Euler limit for every fixed time, while the supremum-over-sets formula passes cumulative inequalities uniformly in the rank s. No finite computation substitutes for this limit.

Rigidity

10. Half-time factor. Q(t)=||S(t/2)1||2 squared, and Q'(t)=-energy(S(t/2)1). The derivative has factor one, not two.
11. Equimeasurability. Weak concentration plus equal squared norms implies equality of distributions by the continuous stop-loss integrals. Equality of total mass alone would not suffice.
12. Energy equality. The already-proved nonnegative heat-content difference has an interior zero at the specified time. Its derivative vanishes there. This yields exact energy equality, avoiding an invalid claim that strict discrete defects survive the Euler limit.
13. Strict concavity. Sub-Markovianity makes the constant-load heat profile decrease in time. Thus Aw>=0; coercivity and positivity show it is nonzero. Applying the positivity-improving semigroup at half time makes Aw>0 on open edges. Spectral smoothing gives edgewise smoothness, so each edge is strictly concave and has at most one critical point. This statement is made only for the constant initial datum.
14. Energy coarea. There are finitely many exceptional values. Coarea gives energies integral a and integral 1/b. Equality plus ab>=N squared implies N=1 almost everywhere. The rearranged profile has the requisite Sobolev representative by the Lipschitz lemma.
15. Topology. Every Dirichlet incidence gives a positive outgoing derivative, so small regular levels count the sum of Dirichlet degrees. It must be one. At a branching standard vertex, zero outgoing derivatives are decreasing incidences by strict concavity. Pigeonhole on increasing/decreasing incidences produces at least two preimages on an interval of levels. The argument covers loop incidences by disjoint small neighborhoods. A connected graph with degree at most two and a leaf is a path.

Corollaries, attribution and limits

The interval eigenfunction expansion was checked analytically: squared constant-function coefficients are 8L divided by pi squared times the odd square. Positive time weighting uses Tonelli and strict pointwise inequality. The torsion constant L cubed divided by three follows directly from the interval quadratic solution. The convex-function comparison is a standard stop-loss integral consequence; it is not counted separately.

Friedlander's energy and branching argument, Vazquez's zero-order comparison and Euler strategy, and the existing torsion result are expressly credited. The mathematical proof contains no computational hypothesis. Markdown/LaTeX checks and PDF inspection concern artifact integrity only. The final source and source-search limitations are in ASSESSMENT.md and source-audit.json. No unresolved proof gap was identified in this internal audit, but external expert scrutiny remains necessary before claiming independent verification.

Revision 1.1 internal proof audit: Section 7

September 16, 2026. Audit by the originating assistant, not independent review.

1. Measures and forms. Rearrangement and heat content use length measure; the separate killing measure may charge vertices. Its finite mass and compact H1-to-C embedding give a closed common-domain form and compact resolvent. Equation (49) supplies a positive spectral gap for kappa > 0. Normal contractions give positivity and sub-Markovianity.
2. Flux sign. Outgoing derivatives point from a vertex into an edge. Their sum is beta times the value. Superlevel integration therefore gives the positive vertex term in (54). The right interval endpoint has outgoing derivative minus v'(L), consistent with Robin coefficient kappa.
3. Cumulative boundary. Global integration gives U(L) + h sum beta u = F(L). The rearrangement endpoint equals the minimum m, so sum beta u >= kappa m = kappa U'(L). The resulting Robin inequality has the correct sign. Its positive-part test contributes positive W_+(L)^2/kappa, as in (52).
4. Preservation of order. The cumulative interval boundary value is G(L), not zero. The argument uses F <= G also at L. This allows induction even when two initial total integrals differ.
5. Regular loads. Strictly positive nonconstant polynomial loads give positive analytic nonconstant edge profiles. Only finitely many critical/vertex levels occur, and the maximum-to-minimum path gives Lipschitz rearrangement. General L2 data follow by density and rearrangement contraction.
6. General measures. Fixed-mass atomic approximations converge weakly on the fixed graph. Uniform convergence against the relatively compact set of H1-unit-ball products gives form-norm convergence (59). Coercivity of the resolvent forms yields H1 convergence (60). The comparison passes first to resolvents and then to evolution; no interchange of two unrelated limits is asserted.
7. Heat limit. Interval iterates remain decreasing. Spectral dominated convergence proves the implicit Euler limit, and cumulative L1 continuity preserves the inequality for every rank and time.
8. Half-time equality. The same self-adjoint identities give equal L2 norms at half time and equal form energies by differentiating the nonnegative heat deficit at its interior zero. Stop-loss equality gives exact equimeasurability.
9. Gradient and killing equality. Piecewise linear approximation extends the classical graph rearrangement energy inequality to H1 functions. The nonnegative difference between potential energy and kappa times the squared minimum then splits equality into two nonnegative defects. The killing measure is supported on the minimum set.
10. Singular-measure regularity. The edge equation gives a measure-valued second derivative. Thus the first derivative is BV and bounded. Strict edgewise concavity of a general killed heat profile is not used and would be false for distributed killing.
11. Critical levels. The Robin comparison profile is positive and strictly decreasing. Its distribution is absolutely continuous between endpoint values and has no endpoint atoms. Equimeasurability gives the same distribution to u. The area formula makes the critical image null, and absolute continuity of the pushforward forces critical-set length zero. Coarea and inverse differentiation therefore lose no mass. Finite multiplicity holds almost everywhere.
12. Topology and measure. Equality forces one preimage at almost every level. Absence of level atoms excludes constant germs. At least three incidences at a vertex give two overlapping same-side level intervals; cycles give two arcs between a minimum and maximum. Thus the graph is a path. Nonmonotonicity on that path would again give repeated levels on an interval. Its minimum is one endpoint, where all killing must be concentrated.
13. Boundary cases. Kappa=0 is excluded because all heat contents equal L. Signed measures and weighted/discontinuous vertex conditions are excluded. Reflection and standard degree-two subdivision preserve equality. The Robin torsion solution (L squared - x squared)/2 + L/kappa gives the constant in (68), which is known for atomic killing.
14. Scope. Separate heat/torsion and spectral comparisons cannot be multiplied to obtain the sharp Kohler-Jobin inequality. No such step is claimed. Finite computation, MathJax checks, PDF rendering and publication are not mathematical certification.

No unresolved proof gap was identified in this internal audit. Independent review and a broader successor-literature audit remain outside the evidence obtained here.

Revision 1.2 internal proof audit: historical Section 8

This section audits the archived one-point proof at commit de0bb20. Its equation numbers refer to revision 1.2, superseded by the general proof below.

1. The first eigenfunction can be chosen nonnegative by form minimization; edge ODE uniqueness and the zero-vertex flux argument make it positive. Strict concavity excludes a minimum at every point except the single killing vertex. Thus m>0 and h=psi-m vanishes exactly there. Cutting at that point need not leave a connected graph; no such hypothesis is used.
2. Superlevel sets exclude the killing point. Flux integration therefore gives a=lambda integral psi, and mu/a <= 1/(lambda m). Analytic nonconstant edge profiles have finitely many critical values. The coarea bound ab>=1 proves tau(t)<=mu(t)^3/3 directly.
3. The trial function L/kappa+g(h) has constant value L/kappa at the sole killing point. The completed-square torsion variational formula gives T>=L squared/kappa+tau. This fails by the same argument for general measures because g(h) need not vanish on their support.
4. In the transplant w(r(t))=P(t), r'=-mu squared/(a r squared) and P'=mu/r. Consequently the gradient energy is preserved exactly, the L1 norm is preserved, and the L2 norm increases because P(t)>=t. The factor two in the layer formula for the squared norm is retained. Truncated energy identities give bounded H1 extension at r=0; no global Lipschitz inverse of the torsion parameter is assumed.
5. Restoring m sqrt(L/R) changes the comparison strength to kappa R/L. Their product in the endpoint energy is exactly kappa m squared. The constant part of the L2 norm is m squared L, and its cross term increases. Keeping strength kappa at this step would be incorrect.
6. For fixed length, logarithmic differentiation of F_s to the power 3/2 yields (87). The difference in (88) has derivative 4 sin(x)(sin(x)-x cos(x)), strictly positive. This proves D>2+(2/3)s rho squared >=2+(2/3)s rho cubed, hence strict decrease of F_s on (0,1].
7. For fixed torsion, K>=tan x and the negative coefficient of K in H_K' allow replacement of K by tan x for an upper bound on the derivative. The residual bracket in (92) has positive derivative sin(u)(3 sin(u)-2u cos(u)). Thus H_K strictly decreases up to arctan K. Interval torsion increases and its first eigenvalue decreases with length at fixed strength, giving (71) in the stated direction.
8. Equality in either scalar comparison forces R=L. The torsion lower bound then meets the already proved sharp upper bound in Corollary 7.2; its equality characterization gives the endpoint-killed interval. Reflection/subdivision gives the converse.
9. Equation (72) has the correct dimensions: b=kappa/sqrt(lambda) is dimensionless, and the interval with that eigenvalue has length arctan(b)/sqrt(lambda). The one-point hypothesis, fixed constraints and general-measure frontier are explicit throughout.
10. Source methods are credited. The numerical diagnostic is not used in either theorem. No unresolved gap was found in this originating-assistant audit; it is not independent mathematical certification.

Revision 1.3 internal proof audit: general-measure Section 8

September 16, 2026. The originating assistant rederived the proof; this is not independent review.

1. Scope and regularization. The coarea proof is first made only for finite atomic measures, after subdivision. The positive ground state is strictly concave on every open edge, so it has finitely many critical points and no positive-length level sets. The extension to arbitrary measures uses common-domain form convergence, not a false assertion of concavity for a ground state with distributed potential.
2. Composition test. For g(0)=0 and G(t)=integral_0^t (g')^2, Cauchy-Schwarz gives g(t)^2 <= t G(t). Nonnegative killing makes the corresponding inequality valid after integrating against nu. The weak eigenvalue test G(psi) identifies the enlarged energy with lambda integral psi G(psi). Fubini gives integral H(g')^2. This is precisely the term missing in the earlier one-point route.
3. Admissibility. The bound H(t)>=lambda m mu(t) makes g and G Lipschitz. Their compositions belong to the continuous H1 form domain. Critical level preimages have zero length in the atomic case, so the Sobolev chain rules are legitimate. No auxiliary massless edge construction is needed in the final proof.
4. Torsion direction. The functional 2 integral v - a[v] is maximized by A^-1 1. Replacing the trial energy by an upper bound produces a lower bound for this functional and hence for T. Choosing g'=mu/H yields (77). No separate torsion upper bound is multiplied by a spectral lower bound.
5. Full flux. Physical level flux plus sum beta_p psi(p) over superlevel vertices equals H. The physical flux alone is at most H. Together with a b>=1 this gives -q'<=lambda U in (79), including levels that pass below killing values. This is the essential sign.
6. Positive-minimum term. Integration over 0<t<m contributes m L^2/(lambda U(L)). The integration-by-parts term at L cancels it; omitting this term would produce an incorrect Dirichlet assertion at small killing. At zero, s^2 q/U tends to zero.
7. Scalar comparison. r=U/q is at least s and satisfies r'<=1+lambda r^2. Integrating the arctangent inequality gives r<=tan(ks)/k only before pi/(2k). Accordingly, z=s/r is between zero and one, and z>=ks cot(ks) on that initial interval. The increasing nonnegative function 2z-z^2 permits dropping the remaining interval. The proof never continues the tangent past its pole.
8. Primitive and constants. The derivative of B(x)=x^3/3+x^2 cot(x) is 2x cot(x)-x^2 cot(x)^2. B(pi/2)=pi^3/24, whose two-thirds power equals the classical graph Dirichlet Kohler-Jobin constant pi^2/24^(2/3). B is strictly increasing because 0<x cot(x)<1.
9. Atomic limit. Weak convergence of measures is uniform against the relatively compact set of products of H1-unit-ball functions. Uniform coercivity gives H1 convergence of torsion solutions. The Rayleigh limsup and compact ground-state liminf prove convergence of the lowest eigenvalues. The scalar bound is continuous at kL=pi/2, so no regularity of a singular-measure ground state is required.
10. Fixed constraints. Rearrangement and potential >= kappa times minimum squared give the independent eigenvalue lower bound (84). For fixed length, kL>=theta then monotonicity of B yields the exact product constant. For fixed torsion, either kL>=pi/2 gives a strictly stronger bound, or k tan(kL)>=kappa gives kL>=arctan(kappa/k). The comparison interval has the original total killing kappa.
11. Equality. Both equalities force kL to equal the appropriate interval angle, hence T=L^3/3+L^2/kappa. Corollary 7.2 then supplies rigidity for arbitrary measures. Thus equality is not inferred by passing equality through an approximation sequence. The endpoint interval verifies every constant directly.
12. Boundary checks. For uniform killing density c, lambda=c and T=L/c; the bound has the correct direction. For an endpoint Robin interval the composition g is linear below its positive minimum, so the Cauchy-Schwarz step is an equality. The weak-killing expansion B(x)=x-x^5/45+O(x^7) is compatible with lambda T approaching L, while the strong-killing limit recovers the Dirichlet constant.
13. Evidence distinction. Reusing 216 saved FEM cases for the new intermediate bound gave no violation. These remain uncertified approximations, with no role in the hand proof. An independent exact limiting example in the research notes disproves a proposed quasiconcavity shortcut; it does not contradict the proved comparison.

No unresolved mathematical gap was identified in this audit. The source comparison credits the classical level-set and Chiti mechanisms, and distinguishes the newly proved general-measure statement from the inaccessible final OT theorem body and the separate Euclidean Robin problem. Publication and artifact checks do not constitute independent certification.

Revision 1.4 internal proof audit: nonlinear Section 9

September 16, 2026. Rederived by the originating assistant; no independent review.

1. Coercivity and normalization. Path Hölder followed by integration against length and nu/kappa proves (95) with constants uniform over all measures of mass kappa. The potential term removes the constant kernel. Strict convexity gives unique torsion. Testing the Euler equation gives E[w]=S_p; scalar optimization gives T_p=S_p^(p-1). Consequently the product exponent is p/d_p for S_p and p/(2p-1) for T_p. These are not interchangeable.
2. Interval calculation. The torsion flux is -x, giving (97) and S_I=L^d/d+L^(p') kappa^(-1/(p-1)). Defining tau_p by the inverse integral gives tau_p'=tau_p^(2-p)(1+tau_p^p). The profile c_p=(1+tau_p^p)^(-1/p) satisfies c_p'=-tau_p c_p and its p-Laplacian equals (p-1)c_p^(p-1). Thus lambda=(p-1)k^p and k tau_p(kL)=kappa^(1/(p-1)). The factor p-1 is necessary.
3. Rearrangement. Coarea Hölder gives alpha_p b^(p-1)>=N^p>=1 for piecewise affine profiles, including graphs with cycles. Approximation and weak lower semicontinuity cover W1p and flat pieces. Potential energy is at least kappa times the pth power of the minimum. The Rayleigh and torsion variational principles give the separate bounds in Lemma 9.2, without multiplying inequalities of incompatible direction.
4. Singular-measure torsion equality. Equality of torsion makes the rearranged minimizer exactly w_I by strict convexity. Both energy defects vanish, and nu lies on the minimum set. The measure-valued flux derivative makes the flux BV and the profile Lipschitz. The interval distribution is absolutely continuous, so the null image of the critical and nondifferentiability set has a null preimage in length. Coarea equality then forces one preimage at almost every level. Branches, cycles and nonmonotonicity each create repeated levels on a value interval. The graph is a path and its minimum is one endpoint. The argument does not assume edgewise concavity under arbitrary killing.
5. Atomic regularity. Subdivide at every killing atom. At a zero of a nonnegative ground state, outgoing fluxes have nonnegative signs and zero sum. Conservation of (p-1)|psi'|^p+lambda psi^p then forces adjacent edges to vanish, contradicting connectivity and normalization. Thus the minimum is positive. Flux derivative is strictly negative on open edges, giving at most one critical point per edge and a finite exceptional level set. This justifies the coarea argument for all p>1, without analytic-ODE assumptions at a vanishing derivative.
6. Composition and torsion direction. H>=lambda m^(p-1) mu makes g and G Lipschitz. Hölder gives g(t)^p<=t^(p-1)G(t); positivity of killing preserves the inequality on integration. The weak eigenvalue test G(psi) then bounds the trial energy from above. Substitution in the torsion supremum gives a lower bound, optimized pointwise by g'=(mu/H)^(1/(p-1)). This proves (106), including levels below the positive minimum.
7. Distribution coordinates. Total superlevel flux includes all positive killing contributions, so the physical flux is at most H. Combining this with coarea Hölder yields -q'<=(lambda U)^(1/(p-1)). The positive-minimum contribution in (108) exactly cancels the integration-by-parts boundary at L. At zero, U(s)/s tends to M^(p-1), making the boundary vanish. The residual integrand is F_p(z)=(p z-z^p)/(p-1), with z=(s/r)^(1/(p-1)) in (0,1].
8. Scalar inverse comparison. Differentiating r=U/q^(p-1) gives r'<=1+((p-1)k r)^(p'). With R=(p-1)kr, substitution u=v^(p-1) in the integrated inequality yields A_p(R^(1/(p-1)))<=ks. Inversion is used only for ks<a_p. Hence z is bounded below by ((p-1)ks)^(1/(p-1))/tau_p(ks). This lower bound is at most one because A_p(t)<=t^(p-1)/(p-1).
9. Primitive and endpoints. Direct differentiation cancels the x^(p') terms in B_p' and gives (111). The scalar F_p is nonnegative and increasing on [0,1]. The identity lambda^(-1/(p-1))=(p-1)^(-1/(p-1)) k^(-p') supplies the remaining factor under x=ks. Thus (112) has exactly k^(-d_p). The part after the pole is dropped only because its original integrand is nonnegative. B_p is continuous at both endpoints and strictly increasing between them.
10. Measure limit. Weak convergence of same-mass measures is uniform on the compact family of |u|^p from a bounded W1p set. Coercivity gives compact minimizing sequences. Rayleigh limsup/liminf proves eigenvalue convergence; the direct method, fixed-test comparison and uniqueness prove torsion-mass convergence. This covers singular continuous measures without assuming regularity of their ground states. The scalar estimate is continuous at the pole.
11. Both constraints and rigidity. For fixed length, the separate spectral comparison gives kL>=theta; monotonicity of B_p proves (93). Equality forces kL=theta and S_p=S_I. For fixed torsion, y=A_p(kappa^(1/(p-1))/k) is below the pole; either kL>=a_p gives strict inequality, or the spectral comparison gives kL>=y. The equal-eigenvalue interval of length y/k has S=k^(-d_p)B_p(y). Interval torsion strictly increases and its eigenvalue strictly decreases with length at fixed kappa. Equality again forces torsion equality at the original graph length, invoking Lemma 9.2 rather than passing equality through approximations.
12. Consistency checks by hand. At p=2, tau_2=tan, d_2=3 and every displayed bound reduces to Section 8. As sigma grows, theta approaches a_p and (93) tends to the cited Dirichlet constant (p-1)a_p^p d_p^(-p/d_p). As sigma tends to zero, theta^p is asymptotic to sigma/(p-1), so the product constant is asymptotic to sigma^((p-1)/(2p-1)), consistent with weak killing. No numerical eigenvalue computation is used in the nonlinear proof.

The final audit found no unresolved gap. The literature methods and nonlinear Dirichlet theorem are credited; the additional claim is the finite-strength nonnegative-measure comparison and its sharp constraints. This internal conclusion does not establish peer review, absolute priority, or the broader extraordinary-conjecture goal. Artifact validation concerns the rendered manuscript only.