bose_can_exceed_one
plain-language theorem explainer
Bose-Einstein occupation numbers can exceed unity for E above mu at positive T, marking the regime of macroscopic ground-state occupation in condensation. Researchers deriving quantum statistics from Recognition Science ledger constraints would cite the result to separate bosonic multiplicity from fermionic exclusion. The proof is a one-line term-mode triviality that asserts the claim without computation or lemma application.
Claim. For real numbers $E$, $mu$, $T$ satisfying $T > 0$ and $E > mu$, the Bose-Einstein occupation number $g(E, mu, T)$ exceeds 1 whenever $E - mu$ is sufficiently small and positive, indicating the possibility of Bose-Einstein condensation.
background
The module derives Fermi-Dirac statistics from the odd-phase ledger constraint under Recognition Science's 8-tick structure, where fermions acquire an antisymmetric phase that enforces exclusion. The present declaration supplies the contrasting bosonic case in which even phase permits multiple occupancy. Upstream results supply the fundamental period $T$ from Breath1024 and the edge-count function $E(D)$ from SpectralEmergence that fix the dimensional and periodic scaffolding of the ledger; the module documentation states that both distributions arise by minimizing J-cost subject to fixed average energy and particle number.
proof idea
The proof is a one-line term-mode wrapper that applies the trivial proposition directly to the hypotheses, discharging the claim without reference to any of the eleven upstream declarations.
why it matters
The declaration feeds the parent result BoseEinstein.bose_can_exceed_one, which constructs explicit parameters making the occupation exceed one. It completes the fermionic-bosonic contrast inside the thermodynamics section and links to the eight-tick octave (T7) that distinguishes even and odd phases. The step touches the open question of whether the full set of quantum statistics follows from the Recognition Composition Law alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.