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

etaBAt

show as:
view Lean formalization →

The definition etaBAt supplies the explicit value of the baryon-to-photon ratio at recognition e-fold N after the GUT epoch as the golden ratio raised to minus N. Cosmologists modeling baryon asymmetry trajectories in the Recognition Science framework cite it as the closed-form phi-ladder descent from unity at N=0. The declaration is introduced by direct abbreviation using the real power operation.

claimLet η_B(N) denote the baryon-to-photon ratio after N recognition e-folds since the GUT epoch. Then η_B(N) = φ^{-N}, where φ is the golden ratio.

background

The BaryogenesisTrajectory module supplies the dynamic half of the matter-consciousness duality theorem. That duality fixes the equilibrium identity η_B · Θ_crit = φ and therefore the present-day value η_B = φ^{-44}. The module adds the trajectory: η_B falls from its GUT-scale value of 1 by exactly one factor of φ^{-1} per recognition e-fold, so that η_B(N) = exp(-N log φ) with N the integer count of e-folds from the GUT epoch.

proof idea

The declaration is a direct definition etaBAt N := phi ^ (-(N : ℤ)). No lemmas or tactics are required beyond the built-in real exponentiation.

why it matters in Recognition Science

etaBAt anchors the certification structure BaryogenesisTrajectoryCert and the supporting theorems etaBAt_pos, etaBAt_44, etaBAt_succ_ratio and etaBAt_strictly_decreasing. It makes the phi-ladder descent explicit, recovering the empirical band at N=44 and aligning with the eight-tick octave and self-similar fixed point of the T0-T8 forcing chain. The definition closes the dynamic content of the module while leaving the origin of the 44-rung gap to upstream results.

scope and limits

formal statement (Lean)

  33def etaBAt (N : ℕ) : ℝ := phi ^ (-(N : ℤ))

proof body

Definition body.

  34
  35/-- η_B is strictly positive at every e-fold. -/

used by (7)

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

depends on (4)

Lean names referenced from this declaration's body.