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)
41noncomputable abbrev rotorPath := IndisputableMonolith.Spiral.SpiralField.logSpiral
proof body
Definition body.
42
43namespace SpiralLemmas
44
45open IndisputableMonolith.Spiral
46
47/-- `logSpiral` is nonzero whenever `r0` is nonzero (since φ^x > 0). -/
depends on (6)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
r0
in IndisputableMonolith.Masses.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
logSpiral
in IndisputableMonolith.Spiral.SpiralField
decl_use