degeneracyPressureExponent
plain-language theorem explainer
DegeneracyPressureExponent sets the non-relativistic degeneracy pressure scaling to the rational 5/3 so that P scales as n to the 5/3. Astrophysicists and stellar modelers cite the value when linking Pauli exclusion to white-dwarf and neutron-star equations of state. The declaration is a direct rational literal with no reduction steps or lemmas required.
Claim. The degeneracy pressure exponent is defined as $5/3$, yielding the non-relativistic scaling $P ∝ n^{5/3}$.
background
The QFT.PauliExclusion module derives the Pauli exclusion principle from ledger single-occupancy for fermions carrying odd phase through the eight-tick cycle. Fermion antisymmetry forces ψ(a,a) = 0, enforcing single occupancy of each quantum state and thereby generating shell capacities together with degeneracy pressure. The module imports SpinStatistics and Constants to support the underlying phase and ledger arithmetic.
proof idea
The declaration is a direct definition that assigns the literal rational 5/3. No lemmas or tactics are invoked; the value is supplied for immediate use by downstream relations.
why it matters
The definition supplies the pressure exponent required by the PauliProofSummary structure, which aggregates all exclusion-principle consequences including shell capacities, the 2n² formula, and the Chandrasekhar limit. It is also referenced by the pressure_energy_relation theorem that equates the exponent to one plus the Fermi-energy exponent. Within the Recognition framework it closes the step from ledger antisymmetry to observable stellar stability bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.