pith. machine review for the scientific record. sign in
theorem proved term proof high

phi_pow_8_upper

show as:
view Lean formalization →

The declaration proves that the eighth power of the golden ratio satisfies φ^8 < 47.03. Cosmologists deriving the baryon asymmetry prefactor η_B in Recognition Science would cite this to fix the upper edge of the washout interval. The proof is a term-mode wrapper that substitutes the Fibonacci closed form for φ^8 and applies the independent bound φ < 1.62 together with linear arithmetic.

claim$φ^8 < 47.03$, where $φ = (1 + √5)/2$ is the golden ratio.

background

The module derives the order-one prefactor c_RS = (1 − φ^{−8})^2 in the baryogenesis formula η_B = c × (integration-gap content). The squared form encodes independent washout of matter and antimatter sectors, each carrying one rung of fermionic degrees of freedom at rate φ^{−8} per fundamental tick in D = 3. The present theorem supplies the concrete upper bound on φ^8 required to obtain the matching lower bound on φ^{−8}.

proof idea

The proof is a term-mode wrapper. It rewrites the left-hand side via the Fibonacci identity theorem phi_pow_8_fib, reducing φ^8 to the linear expression 21φ + 13. It then introduces the hypothesis φ < 1.62 from the upstream lemma phi_lt_onePointSixTwo and closes immediately with linarith.

why it matters in Recognition Science

This bound is invoked directly by the downstream theorem phi_zpow_neg8_lower to establish φ^{−8} > 0.02126. The pair of bounds pins φ^8 inside (46.81, 47.03) and thereby anchors the predicted interval (6.0 × 10^{−10}, 6.2 × 10^{−10}) for c_RS · φ^{−44}, which matches the Planck 2018 value of η_B. In the framework it instantiates the eight-tick octave (T7) at D = 3, providing the numerical anchor for the washout factor inside the Recognition Composition Law application to baryogenesis. The squared interpretive form of c_RS remains hypothesis-grade.

scope and limits

Lean usage

have hupper : phi ^ (8 : ℕ) < 47.03 := phi_pow_8_upper

formal statement (Lean)

  70theorem phi_pow_8_upper : phi ^ (8 : ℕ) < 47.03 := by

proof body

Term-mode proof.

  71  rw [phi_pow_8_fib]
  72  have hphi : phi < 1.62 := phi_lt_onePointSixTwo
  73  linarith
  74
  75/-! ## φ^(−8) bounds -/
  76

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.