pauli_bound_very_small
plain-language theorem explainer
The theorem shows that the predefined Pauli violation bound of 1/10^29 is strictly less than 1/10^20. Quantum field theorists and experimentalists testing fermion statistics would cite it to quantify the empirical tightness of the exclusion principle. The proof is a direct term reduction that unfolds the constant definition and applies numerical normalization.
Claim. The experimental upper bound on Pauli violation probability per electron pair satisfies $1/10^{29} < 1/10^{20}$.
background
The QFT.PauliExclusion module derives the exclusion principle from Recognition Science ledger single-occupancy. Fermions are odd-phase entries in the 8-tick cycle; antisymmetry then forces any two identical fermions sharing a state to cancel, yielding zero amplitude and single occupancy. The module links this to atomic shell structure and the periodic table.
proof idea
The term proof unfolds pauliViolationBound to the constant 1/10^29 and applies norm_num to confirm the numerical inequality holds.
why it matters
The result anchors the empirical side of the ledger-derived exclusion principle within the Recognition Science framework, confirming that violations remain below any detectable threshold. It supports downstream module claims on subshell capacities and shell filling. The bound aligns with the T7 eight-tick octave and odd-phase accumulation for fermions; no open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.