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

phiContinuedFraction

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 130def phiContinuedFraction : List ℕ := [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]

proof body

Definition body.

 131
 132/-! ## The J-Cost Connection -/
 133
 134/-- In RS, e appears in probability distributions:
 135
 136    Boltzmann: P ∝ exp(-E/kT)
 137    J-cost: P ∝ exp(-J/J₀)
 138
 139    The exponential (base e) is fundamental for probability normalization.
 140
 141    Why e specifically? Because:
 142    d/dx e^x = e^x
 143
 144    Only exponential maintains shape under differentiation. -/

depends on (12)

Lean names referenced from this declaration's body.