The convolution-stable body B_k

For a probability distribution with sorted atoms p₁↓ ≥ p₂↓ ≥ … ≥ p_k↓, the body B_k is defined by p_k↓ ≥ (1 − p₂↓ − (1 − p₂↓)^k)/(k − 1).

Main theorem (stability). For every k ≥ 4, additive convolution preserves B_k on every finite abelian group of order k, and multiplicative convolution preserves it on every finite field of that order.

The formalization proves the sharper algebraic statement suggested by the permutation argument: convolution for any finite quasigroup operation preserves B_k. It also covers an operation with an absorbing zero whose nonzero part is a quasigroup, so the field multiplication theorem is a special case. No associativity, commutativity, identity, inverse, or compatibility between the two operations is needed.

The body is full-dimensional, contains the point masses and the uniform law, and has an explicit normalized-volume formula with a sharp exponential scale.

The paper is all_q_standalone.tex, with the rendered artifact at output/pdf/read_once_value_distributions.pdf.

Lean formalization

The Rronce/ library machine-checks the stability and geometric theorems on top of Mathlib. Its proof chain uses no sorry, no native_decide, and no new axioms; the exported endpoints depend only on propext, Classical.choice, and Quot.sound. (The Lean development retains the letter q for the field order in its identifiers and statements; the paper now writes k.)

Finished, kernel-only:

• the B_k addition gate for every k ≥ 4, over any finite abelian group (Rronce.Bq.add_gate_preserves_Bq);
• the B_k multiplication gate for every finite field of order k ≥ 4 (Rronce.Bq.mul_gate_preserves_Bq);
• the quasigroup extension of both gates: every operation whose left and right translations are permutations preserves B_k, as does every absorbing-zero operation with that property off zero (Rronce.Bq.quasigroup_conv_preserves_Bq, zero_quasigroup_conv_preserves_Bq, and the combined quasigroup_gates_preserve_Bq);
• the read-once application: over every finite field of order k ≥ 4, the exact rational value distribution of every read-once formula on independent uniform inputs lies in B_k (Rronce.General.main_membership_qge4); the derived inequality p₁↓ − p_k↓ ≤ (1 − p₂↓)^k holds over every finite field of order ≥ 2 (Rronce.General.main_conjecture_qge2, with the historical q ≥ 4 formulation retained as main_conjecture_qge4);
• geometric nonvacuity of B_k: the uniform vector is an ambient interior point, with an explicit sup-norm ball of radius (k-1)^(k-1) / (2*k^k) contained in the invariant (Rronce.Bq.uniformVector_mem_interior_memBq);
• the quantitative normalized-volume bound vol(B_k)/vol(Δ_(k-1)) ≥ ((k-1)^(k-1)/(2*k^k))^(k-1) > 0 for closed Borel chart sets (Rronce.Bq.volume_fraction_measurable, volume_fraction_lower_bound, and volume_fraction_positive);
• the exact normalized volume and its sharp exponential scale: an explicit one-dimensional inclusion--exclusion integral (Rronce.Bq.exact_volume_formula), together with log(vol(B_k)/vol(Δ_(k-1)))/k → Λ_* and the equivalent root limit (vol(B_k)/vol(Δ_(k-1)))^(1/k) → exp(Λ_*) = 0.2183305369... (Rronce.Bq.exact_volume_exponential_asymptotics and exact_volume_root_asymptotics), where the exact rate is selected by a proved-unique positive saddle.

Build / verify (Lean v4.32.2, Mathlib v4.32.2, both pinned in lean-toolchain / lake-manifest.json):

lake exe cache get      # fetch the Mathlib build cache
lake build              # builds the whole library
lake env lean AxiomCheck.lean   # restates the endpoints; prints trust base

AxiomCheck.lean restates each finished theorem against its frozen statement file (so it only typechecks with no hidden weakening) and #print axioms reports the exact trust base.

Library layout (Rronce/)

• Bq/ — the invariant body: frozen gate statements (Statement.lean, MulStatement.lean, and the proof-free quasigroup extension QuasigroupStatement.lean), the machine-checked addition theorem (AddProof.lean/AddGate.lean), and the completed all-q multiplication proof (Mul/, assembled by MulProof.lean and exposed by MulGate.lean). The generalized proof is assembled in QuasigroupProof.lean and exposed by QuasigroupGate.lean. The directory also contains the explicit full-dimensionality certificate for the invariant body (Nonvacuity.lean) and the normalized-volume theorem (VolumeStatement.lean is proof-free, VolumeProof.lean supplies the proof, and Volume.lean is the public header). The exact integral and asymptotic rate are frozen separately in the proof-free ExactVolumeStatement.lean; the clipped-cube, order-statistic, scaling, exponential-tilt, concentration, and Stirling proofs live under Bq/ExactVolume/, are assembled by ExactVolumeProof.lean, and are exported by ExactVolume.lean.
• General/ — the read-once application: frozen formula and probability statements (Statement.lean, AllOrdersStatement.lean, GateReductionStatement.lean), the recursive-law semantics with the read-once identification and B_q induction, and the public endpoints exposed by AllOrders.lean.
• Q4/Statement.lean — the frozen historical q = 4 specialization, retained for audit compatibility. The original certificate-based q = 4 proof (Q4/Distribution/, RealLift/, certs/; ~15M lines of generated interval-arithmetic certificates discharged by native_decide) has been removed from the working tree for digestibility once the analytic all-q route made it redundant; it is preserved in git history (commit 2448df8 and earlier).

Paper

• all_q_standalone.tex — the paper: the body B_k, its exact normalized volume and sharp exponential scale, the addition and multiplication gate theorems and their quasigroup strengthening, scalar endpoint appendices, and a Lean formalization appendix listing the audited endpoints, with the main Lean statements reproduced verbatim in a final appendix.
• output/pdf/read_once_value_distributions.pdf — the rendered and visually checked paper.
• Historical development notes, exploratory searches, and the obsolete q = 4 TeX/certificate atlas have been removed; git history preserves them.

The paper source is a single self-contained file. Build with:

mkdir -p output/pdf
pdflatex -interaction=nonstopmode -halt-on-error \
  -jobname=read_once_value_distributions \
  -output-directory=output/pdf all_q_standalone.tex
# Run the same command once more to stabilize references.

License

The Lean development and all repository content are released under the Apache License 2.0, matching the Lean 4 and Mathlib convention.