🧠 mindful(t), entries in logic

∀t, mindful(t)

🌀

structure 📒LeanLog :=
  (t : Title) (φ : Prop) (e : Expr)
  (🖊 : Sketch) (🌈 : List Sensory)
  (🪞 : Comment)

b/b ~ basic building blocks

example (a : Nat) : a = a := rfl

I wondered if music can be written mathematically, can mathematics be written musically? #question

I conjecture with Lean4 snippets we might gain insight to how mathematics is musical as well as how music is mathematical!

x = x is #maybe similar to playing C∆7inversions monotonously on every quarter note.

by adding change, variability, you could maybe play different roots, base notes with C∆7 as upper structure:

A × C∆7 ⟶ D × C∆7 ⟶ G × C∆7.

Vamp ↻ #

C₁ ⟶ C₂ ⟶ ... ⟶ Cₙ
 ↑                 ↓
 └──────loop───────┘

structure Vamp (C : Type) :=
(chords : List C)
(repeat : Bool := true)

🪐

{α} ⇒ ∅ holds iff contradiction {α} ⇒ ∅ doesn't hold iff satisfiable