bose_from_even_phase
plain-language theorem explainer
The theorem establishes that the phase factor at zero ticks equals unity, encoding the symmetric exchange property for bosons and permitting multiple occupancy per state. Researchers deriving Bose-Einstein statistics from Recognition Science would cite this when linking the eight-tick structure to the minus sign in the occupation factor. The proof is a direct term pairing the zero-phase identity with a trivial conjunction.
Claim. The phase exponential at zero ticks satisfies $e^{i k} = 1$ where $k = 0$ in the eight-tick sequence, confirming the symmetric weight that allows arbitrary occupation numbers and produces the Bose-Einstein form $g(E) = 1/ (e^{(E - μ)/T} - 1)$.
background
The module connects J-cost minimization to thermodynamic distributions through eight-tick phases. The phase map assigns values $k π / 4$ for integer $k$ from 0 to 7, and its complex exponential yields the exchange sign. Upstream results include the definition of these phases and the explicit theorem that the zero case returns exactly 1, corresponding to the identity under particle exchange for bosons.
proof idea
The proof is a one-line term wrapper that applies the zero-phase identity lemma together with the trivial proposition for the conjunction.
why it matters
This supplies the even-phase identity required by the Bose-Einstein theorem in the downstream BoseEinstein module. It completes the even-phase step in the spin-statistics derivation from the eight-tick octave, directly producing the minus sign in the Bose-Einstein denominator as stated in the module documentation. The result anchors the J-cost bridge to standard quantum statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.