261 "No known simple e = f(φ) formula", 262 "φ: discrete; e: continuous", 263 "Connected through complex exponential", 264 "J-cost normalization requires e", 265 "e: unique self-similar exponential base" 266] 267 268/-! ## Falsification Criteria -/ 269 270/-- The derivation would be falsified if: 271 1. A simple e = f(φ) formula is found 272 2. Some other base works for J-cost 273 3. e is not required for normalization -/
depends on (12)
Lean names referenced from this declaration's body.