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

rsInterpretation

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)

 233def rsInterpretation : List String := [

proof body

Definition body.

 234  "Probabilities: exp(-J) for cost-weighted",
 235  "Time evolution: exp(iωt) for 8-tick phases",
 236  "Growth limit: e maximizes (1+1/n)^n",
 237  "Normalization: Required for consistency"
 238]
 239
 240/-- Why e and not some other base?
 241
 242    Because d/dx b^x = b^x × ln(b)
 243
 244    Only for b = e: d/dx e^x = e^x
 245
 246    This self-similarity is required for J-cost evolution. -/

used by (1)

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

depends on (15)

Lean names referenced from this declaration's body.