Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Score Bounds at Envelope Test Inequalities from the Absorption Slack
lemmalem:nc-envelope-score-bounds-2026aAnalysisProbabilityFor a Hamiltonian that absorbs shifts at the noise level and is bounded at zero momentum at bounded positions, a momentum shift that satisfies either envelope test inequality at a bounded position has norm at most a constant over the shift size, with the admissible shift sizes de…The Wall-Confined Free Energy Converges along Wasserstein-Convergent Sequences with Bounded Scores
lemmalem:nc-energy-convergence-bounded-scores-2026aAnalysisProbabilityIf laws in the score domain converge in the Wasserstein distance to a law in the domain and their scores stay bounded in L^2, then their wall-confined free energies converge to the free energy of the limit.The Coupling Test Function of a Bounded Plan: Maximising Couplings, Continuity, Plan Subjets and Localisation
lemmalem:nc-coupling-test-function-2026aAnalysisProbabilityFor a bounded plan at a bounded law, the coupling test function built from a differentiable gauge with vanishing derivative at zero and a quadratic weight is attained by a maximising coupling, is Wasserstein-continuous on bounded laws, and admits an explicit plan subjet read off…The Score Plan of a Law in the Score Domain of the Wall-Confined Free Energy
definitiondef:nc-score-plan-2026aAnalysisProbabilityThe score plan of a law in the score domain is the joint law of the position variables and the score, a square-integrable law of 2d variables.- If two plans realised on a common position tuple are plan superdifferentials (or subdifferentials) of two functions with given slacks, then the plan with the summed momenta is a plan superdifferential (or subdifferential) of the sum, with the summed slack.
Gluing Countably Many Square-Integrable Noncommutative Laws along a Common Marginal
lemmalem:l2-countable-gluing-common-marginal-2026aAnalysisProbabilityCountably many square-integrable noncommutative laws that share the law of their first k variables are realised jointly in one tracial W*-probability space, by one common k-tuple and one further tuple for each law.A Nondecreasing Differentiable Majorant with Vanishing Derivative at Zero for a Little-o Modulus
lemmalem:little-o-differentiable-majorant-2026aAnalysisA bounded nonnegative function on an interval [0,r] that vanishes faster than linearly at zero lies below a nondecreasing, differentiable function on the half-line that vanishes at zero, with bounded derivative tending to zero at zero.Envelope Viscosity Solutions versus Free-Energy-Penalised Viscosity Solutions: Envelopes of Semicontinuous Functions, and Semicontinuous Envelope Solutions are Penalised Solutions under Absorption
lemmalem:nc-envelope-penalised-bridge-2026aAnalysisPDEFor a Wasserstein upper semicontinuous function the upper penalty envelope is the function minus delta times the free energy (and dually); consequently, when the Hamiltonian absorbs shifts, a semicontinuous envelope subsolution or supersolution is also a free-energy-penalised one…Shift-Convergent Sequences of Positions, Momenta and Shifts in a Tracial W*-Probability Space
definitiondef:nc-shift-convergent-sequence-2026aAnalysisProbabilityIn one tracial W*-probability space: positions with laws of norm bound r converging in L^2, momenta converging in L^2, and bounded shifts converging weakly.Comparison, Uniqueness and Continuity on Energy Sublevel Sets for Envelope Viscosity Solutions of the Discounted HJB Equation with Free Langevin Noise in a Wall
theoremthm:nc-envelope-comparison-2026aAnalysisPDEWithout any semicontinuity assumption, a bounded envelope subsolution lies below a bounded envelope supersolution on the domain of the free energy; bounded envelope solutions are unique and automatically Wasserstein-continuous on every sublevel set of the free energy.Comparison at a Fixed Level for Envelope Viscosity Solutions of the Discounted HJB Equation with Free Langevin Noise in a Wall
lemmalem:nc-envelope-fixed-level-comparison-2026aAnalysisPDEAt each fixed level delta, the upper penalty envelope of a bounded envelope subsolution lies below the lower penalty envelope of a bounded envelope supersolution up to an error e(delta) that tends to zero with delta and depends only on the sup-norm bound and the data.Envelope Viscosity Subsolutions, Supersolutions and Solutions of the Discounted HJB Equation with Free Langevin Noise in a Wall
definitiondef:nc-envelope-viscosity-solution-2026aAnalysisPDEAt each level delta up to a shift range, test the penalty envelope of u by strict extrema against arbitrary test functions with plan jets; at such a point the law must have a score, and the equation must hold with the momentum shifted by delta times the score, keeping the good te…The Discounted HJB Equation with Free Langevin Noise in a Wall, Envelope Form: Standing Notation
settingset:nc-envelope-hjb-2026aAnalysisPDEStanding notation for the envelope theory of the free Langevin HJB equation in a wall: the data of the penalised setting, the Wasserstein metric on the domain, self-adjoint scores and shifted plans, and the penalty envelopes of bounded functions.Shift Semicontinuity of a Hamiltonian on Phase-Space Noncommutative Laws
definitiondef:nc-hamiltonian-shift-semicontinuity-2026aAnalysisPDEAlong strongly convergent bounded positions and momenta and weakly convergent bounded shifts in one tracial W*-probability space, the Hamiltonian with an upward shift plus the good quadratic term is lower semicontinuous, and with a downward shift minus that term is upper semicont…Absorption of Shifts by a Hamiltonian on Phase-Space Noncommutative Laws
definitiondef:nc-hamiltonian-shift-absorption-2026aAnalysisPDEA Hamiltonian absorbs shifts at noise level sigma if, at bounded positions, shifting the momentum by delta Q changes it by at most delta times a function of the momentum norm plus a quarter of sigma squared delta times the squared norm of Q, for all small delta.The Penalty Envelopes of a Bounded Function on the Domain of the Wall-Confined Free Energy
definitiondef:nc-penalty-envelopes-2026aAnalysisPDEFor a bounded function u and a level delta > 0, the penalty envelopes are the Wasserstein upper semicontinuous envelope of u minus delta times the free energy and the lower semicontinuous envelope of u plus delta times the free energy, on the domain of the free energy.The Shift of a Bounded Plan by a Self-Adjoint Field
definitiondef:nc-plan-shift-2026aAnalysisProbabilityShifting a bounded plan (a joint law of positions and momenta) by t times a self-adjoint field on the position law adds t times the field to the momenta in the canonical realisation of the plan; the result is a square-integrable law of 2d variables.Conjugate Variables, Wall Forces and Scores are Square-Integrable Tuples of the GNS Space
lemmalem:nc-score-self-adjoint-2026aAnalysisProbabilityThe conjugate variables of a noncommutative law, its square-integrable wall force and hence the score of the wall-confined free energy consist of vectors fixed by the conjugation, so they are square-integrable tuples of the law's tracial W*-probability space.Comparison and Uniqueness under Wasserstein Semicontinuity for the Controlled von Neumann HJB Equation with Free Langevin Noise in a Wall, Including the Free Entropy Penalty
corollarycor:nc-von-neumann-comparison-w2-2026aAnalysisPDEFor the controlled von Neumann HJB equation with free Langevin noise in a wall and a uniformly continuous running cost, a bounded Wasserstein-upper-semicontinuous penalised subsolution lies below a bounded Wasserstein-lower-semicontinuous penalised supersolution on the wall domai…The Controlled von Neumann Hamilton-Jacobi-Bellman Equation with Free Langevin Noise in a Wall on Noncommutative Laws
equationeq:nc-von-neumann-hjb-2026aAnalysisPDEThe discounted HJB equation with free Langevin noise in a wall whose Hamiltonian is the controlled von Neumann Hamiltonian, written in score form.