E_coh_pos
plain-language theorem explainer
The lemma shows that coherence energy E_coh is strictly positive in RS-native units, where it equals phi to the power minus five. Workers on vacuum energy bounds or gauge alignment cite it to secure positivity in downstream energy expressions. The proof is a one-line wrapper that invokes the positivity result for the locked lag constant cLagLock.
Claim. $0 < E_ {rm coh}$, where the dimensionless coherence energy is defined by $E_{rm coh} := phi^{-5}$.
background
The Constants module works in RS-native units with tau_0 equal to one tick and ell_0 equal to one voxel. Coherence energy is introduced as the definition E_coh := cLagLock, which equals phi to the power minus five by the Phase 2 derivation. The upstream lemma cLagLock_pos states that 0 < cLagLock and proves it by unfolding the definition then applying Real.rpow_pos_of_pos to the fact that phi is positive.
proof idea
The proof is a one-line wrapper that directly applies the lemma cLagLock_pos.
why it matters
This result is invoked by the vacuum energy positivity theorem, which concludes phaseLockEnergy > 0 from the product of passive_fraction_pos and E_coh_pos. It also appears inside the phi forcing principle, which lists 0 < E_coh among the forced properties of the self-similar ledger. The positivity therefore supports the constant derivations that feed the T5-T8 forcing chain and the mass-ladder expressions used in sector yardsticks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.