no_pauli_violation_observed
plain-language theorem explainer
The declaration shows that the defined Pauli violation bound of 1/10^29 lies strictly below 10^{-28}. Precision tests of quantum statistics and atomic stability calculations would cite this numerical confirmation. The proof is a one-line wrapper that unfolds the bound definition and applies norm_num to the resulting rational inequality.
Claim. The experimental bound on Pauli violation probability per electron pair satisfies $1/10^{29} < 1/10^{28}$.
background
The module derives the Pauli exclusion principle from Recognition Science ledger single-occupancy: fermions are odd-phase entries under the eight-tick cycle, so identical states produce antisymmetric wavefunctions that must vanish at coincidence, enforcing one fermion per quantum state. This yields shell capacities 2, 6, 10, 14 and degeneracy pressure scaling as n^{5/3}. The upstream pressure definition returns ρ times the kernel evaluation times δ, supplying the effective source term 4π G a² p. The for structure records the meta-realization axioms needed for self-reference coherence. The bound constant itself is fixed at the rational 1/10^{29}.
proof idea
Unfold pauliViolationBound to obtain the explicit rational 1/10^{29}, then invoke norm_num to discharge the comparison 1/10^{29} < 1/10^{28}.
why it matters
The result supplies the experimental closure for the ledger-derived Pauli principle and supports the PRB paper on first-principles atomic shell structure. It sits inside the eight-tick octave (T7) that assigns the odd phase to fermions and feeds the degeneracy-pressure and Chandrasekhar-limit statements listed in the module summary. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.