E_coh_pos
plain-language theorem explainer
E_coh is strictly positive in RS-native units. Researchers deriving constants along the phi-to-alpha chain cite this to guarantee the coherence quantum has positive sign before multiplication in vacuum energy or forcing axioms. The proof is a one-line term reduction that unfolds the definition and invokes positivity of integer powers on a positive base.
Claim. $0 < E_coh$ where $E_coh := phi^{-5}$ in RS-native units and $phi > 1$ denotes the golden ratio.
background
The RRF Foundation module derives all constants from phi via gate identities, with the explicit chain phi to E_coh to tau_0 to c to hbar to G to alpha inverse. E_coh is introduced as the coherence energy E_coh = phi^{-5} (approximately 0.09 eV in calibrated units). Upstream results in ConstantDerivations and PhiForcing establish the identical positivity statement by the same reduction, while the module doc-comment records the IR gate hbar = E_coh * tau_0 as the immediate downstream identity.
proof idea
The term proof unfolds E_coh to the expression phi ^ (-5 : Z) and applies the library lemma zpow_pos to the hypothesis phi_pos that the golden ratio is positive.
why it matters
This result supplies the positivity hypothesis required by vacuum_energy_pos in Cosmology.VacuumUniformity (via mul_pos with passive_fraction_pos) and by the phi_forcing_principle theorem, which lists 0 < E_coh among the axioms of the forcing chain. It therefore closes the basic sign check for the coherence quantum in the T5-T8 sequence and in the RCL composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.