E_coh_pos
plain-language theorem explainer
The lemma asserts that cohesion energy E_coh is strictly positive. Workers on vacuum energy bounds, gauge alignment, and the phi forcing principle cite it to guarantee non-negative derived energies. The proof is a one-line term wrapper that forwards directly to the corresponding positivity result in the main Constants module.
Claim. $0 < E_coh$, where $E_coh$ is the cohesion energy expressed in RS-native units.
background
The Compat.Constants module supplies project-wide constants and minimal structural lemmas in RS-native units (c=1, ħ=phi^{-5}). E_coh is defined as a placeholder cohesion energy re-exported from the main Constants module. Upstream lemmas establish positivity via the explicit relation E_coh = phi^{-5}, using the fact that phi > 1 implies zpow_pos phi_pos (-5).
proof idea
Term-mode one-line wrapper that applies the E_coh_pos lemma from IndisputableMonolith.Constants (itself proved by unfolding E_coh and invoking zpow_pos phi_pos (-5)).
why it matters
This result is invoked by vacuum_energy_pos (which multiplies it by passive_fraction_pos), phi_forcing_principle (which lists 0 < E_coh among the forcing axioms), and gauge_alignment_possible (which scales sector gauges by E_coh). It closes a link in the T5-T8 forcing chain by ensuring the coherence quantum remains positive, supporting the eight-tick octave and mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.