E_coh_pos
plain-language theorem explainer
The theorem proves that the coherence quantum E_coh, defined as phi to the power minus five, is strictly positive. Researchers deriving vacuum energy bounds or coherence scales in Recognition Science cite this when establishing positivity at the phi-forcing step. The proof is a direct term-mode reduction that unfolds the definition and applies zpow_pos to the known positivity of phi.
Claim. $0 < E_ {rm coh}$ where $E_{rm coh} := phi^{-5}$ and $phi = (1 + sqrt{5})/2$ is the golden ratio.
background
The PhiForcing module shows that phi arises as the unique positive solution to the self-similarity equation x^2 = x + 1 inside a discrete J-cost ledger. E_coh is introduced here as the coherence quantum with the explicit definition E_coh := phi^{-5}. This choice matches the RS-native unit convention in which fundamental scales appear as negative powers of phi. The module doc states that phi is forced by self-similarity in a discrete ledger with J-cost, building on the Composition law and J-uniqueness from earlier levels of the forcing chain. Upstream, phi_pos is supplied by ConstantDerivations and the zpow_pos lemma is available from Mathlib.
proof idea
The proof is a term-mode one-liner. It first simplifies the definition of E_coh with simp only [E_coh], then applies the lemma zpow_pos directly to the hypothesis phi_pos at exponent -5.
why it matters
This positivity result is invoked inside the PHI FORCING PRINCIPLE theorem of the same module, which packages the golden equation, uniqueness of phi, and the positivity of both J_bit and E_coh. It is used downstream by vacuum_energy_pos in Cosmology.VacuumUniformity and by gauge_alignment_possible in SectorYardsticks. Within the forcing chain it supplies the required positivity at the phi-forcing step (T6) before the derivation of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.