pith. machine review for the scientific record. sign in
theorem proved term proof

dimensions_from_log

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)

  93theorem dimensions_from_log : dimensionsFromTicks = Nat.log 2 8 := by

proof body

Term-mode proof.

  94  native_decide
  95
  96/-- The correspondence:
  97    - Dimension 0 (x) ↔ Generation 1 (lightest)
  98    - Dimension 1 (y) ↔ Generation 2 (medium)
  99    - Dimension 2 (z) ↔ Generation 3 (heaviest)
 100
 101    This is a structural correspondence, not a dynamical one. -/

depends on (16)

Lean names referenced from this declaration's body.