building R from scratch

• 12 August 2025
• Mathematics,
• Process book,
• Learning

skankin' R 🎷 #

I have

class R (a : Type) where
  zero : a
  one : a
  add : a → a → a
  mul : a → a → a

and error messages
--It's maybe a bit like building an app, a code, a project, something, a portfolio project
  I rebuilt R and sin x

#restorative

Before checking, pause 3 s, exhale, soften shoulders 
— make this the actual goal.

structure FinancialState :=
  (income : ℝ)
  (expenses : ℝ)
  (savings : ℝ)

wow e and sin are growth 🌱 & waves 🌊

def proof {A B : Prop} (f : A → B) : A → B := f
structure Lin (V W : Type) := (map : V → W)

🎶timbre:
bright → exp,
nasal → sin.s

def zork (r : R) (blip : r) := (neg := fun x => ???, inv := fun x => ???) 
-- guess: zork blip -> (neg blip, inv blip)

🎨

def frotz(zo, bl):
  return ("neg", -bl), ("inv", 1/bl)
# guess output?

🪴

struct Q{int gl;}; struct Q goop(struct Q q){q.gl=-q.gl; return q;}
/* guess resulting q.gl */

🥕

def glorp {a} [R a] (x y : a) :=
  (add x (neg y), mul (inv x) y)
-- guess: what does `glorp 4 2` produce in ℝ?

♾️

def snarf(a,b):
    return (a - b, b / a)
# guess: snarf(5,10)?

♩

--I definitely had an aha moment here, struggling with the first Lean4 more abstract definition, then seeing the Python one clarity ensued! 🎉

🤖🌿 That’s exactly the magic ✨ — kleine „Aha“-Erlebnisse 🐚 turn foggy abstractions into clear shapes. It’s like suddenly spotting the lighthouse 🗼 while sailing at night ⛵ — same waters, but now you see the route.

🐙 Your R is nearly ready, but you’ll want:

• Fix type var: use a instead of r in field types.
• Maybe add sub and div as derived ops from add+neg and mul+inv.
• Possibly include eq or decidable equality for comparisons.

add+neg and mul+inv are sub, and div, so cool! 😌

In my experience it is much nicer to learn this way, because I used to struggle to see these patterns in textbooks, and now while thinking about these puzzles, and components of constructing R from scratch I remember more readily... (maybe the struggle to see these patterns through textbooks helps with now learning it easier? Like "Oh finally I have a means to learn these things...)
  Like "Oh what do I need to be able to use exp"?
   I needR, which is a Type with add, zero, one ...

“What do I need for exp?”
🦆 You cracked it — a ring-like R with add, zero, one, mul, neg, inv.

e - Cracked ✔ 🎉
  (exp still seems terribly complex for me (🐒✨ "YET"))

x^n/n! is very similar to sin x, are they the same function?
exp grows, sin waves back and forth

∑

def floop (x : Float) (N : Nat) := 
  List.range (N+1).sum (λ n => x^n / Nat.factorial n)  
# guess floop 1 3?  

--λ n => x^n, how is n changed, it ranges over, iterated over range(3)?

🤖🌿 Exactly! λ n => x^n / n! is applied for each n in List.range (N+1) = {0,1,2,3} here, then summed. So n iterates over 0 to N, producing terms in the series.

🐵 "Is this the categonified version?"

🐈‍⬛✨ Yes! The function λ n => x^n / n! is a morphism from the discrete category of natural numbers (0 → 1 → 2 → ...) into your numeric type, then combined by colimit (sum).
Think:

• Objects: indices n
• Morphisms: ordering n≤m
• Functor: sends n↦xn/n!
• Colimit = sum over all n — a categorial fold! 🧶⛵️

--I'm confused, is this word soup?

🐛 bruv

References #

I was inspired by the gibberish variables idea in Think Python. by Allen B. Downey

• Previous: arrow only categories
• Next: Term Theory