pauliViolationBound
plain-language theorem explainer
The definition supplies the numerical upper bound of 1 over 10 to the 29 on Pauli violation probability per electron pair. Experimentalists testing quantum statistics and theorists linking exclusion to ledger single-occupancy would cite the constant when comparing theoretical predictions to measured limits. It is introduced as a direct rational constant assignment with no computation or lemmas required.
Claim. The experimental bound on the probability of Pauli violation per electron pair is $1/10^{29}$.
background
In the QFT module on Pauli exclusion the principle is derived from ledger single-occupancy: fermions are odd-phase entries that accumulate a minus sign through the 8-tick cycle, so that two identical states at the same address would require ψ(a,a) = −ψ(a,a) and therefore force ψ(a,a) = 0. This single-occupancy constraint produces atomic shell structure, the periodic table, and degeneracy pressure. Upstream results establish collision-free ledger properties and algebraic identities that underwrite the antisymmetry step.
proof idea
The definition is a direct assignment of the rational constant 1/10^29. No lemmas are invoked and no tactics are executed; the value is fixed for use in downstream comparisons.
why it matters
The bound anchors the two immediate theorems that conclude no Pauli violation has been observed and that the bound is very small. It supplies the numerical link between the ledger-derived exclusion principle (odd-phase 8-tick entries, single-occupancy) and experimental limits, supporting the paper proposition on first-principles derivation of atomic shell structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.