pith. machine review for the scientific record. sign in
def definition def or abbrev high

E_coh

show as:
view Lean formalization →

E_coh sets the coherence energy to phi to the power of minus five in RS-native units. Mass derivations on the phi-ladder cite this scale when fixing the base energy for rung calculations. The definition is a direct substitution once the coherence exponent is fixed at five by the relation octave minus D.

claim$E_{coh} := phi^{-5}$ in RS-native units, where the exponent equals the Fibonacci deficit $2^D - D$ evaluated at the unique dimension $D=3$ that satisfies the octave constraint.

background

The module derives the coherence energy exponent from the Fibonacci constraint that both $D$ and $2^D$ must be Fibonacci numbers. This forces $D=3=F_4$ and $2^D=8=F_6$, so the deficit $8-3=5=F_5$ supplies the exponent. The sibling definition coherence_exponent computes octave minus D, while the imported Constants structure supplies the base value of phi. The upstream Physics.ElectronMass.Defs version states the same deficit explicitly as $2^D - D$.

proof idea

One-line definition that raises Constants.phi to the integer power given by the negative of coherence_exponent. The cast to ℤ is required only for the exponent type; the value is already fixed at five by the Fibonacci identities proved elsewhere in the module.

why it matters in Recognition Science

This definition supplies the concrete energy scale phi^{-5} that enters every mass formula of the form yardstick times phi to a rung offset. It realizes the module's main claim that the exponent is not free but is fixed by the Fibonacci selection of D=3 and the eight-tick octave. The result therefore anchors the T7-T8 segment of the forcing chain and the mass-ladder construction.

scope and limits

formal statement (Lean)

 133noncomputable def E_coh : ℝ := Constants.phi ^ (-(coherence_exponent : ℤ))

proof body

Definition body.

 134
 135/-- E_coh = φ^{-5} -/

depends on (3)

Lean names referenced from this declaration's body.