def definition def or abbrev

`FieldVelocity`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  46def FieldVelocity (r : ℝ) (n_coils : ℕ) (pulse_width : ℝ) : ℝ :=

proof body

Definition body.

  47  (2 * Real.pi * r) / (n_coils * pulse_width)
  48
  49/-- RS Hypothesis: Relativistic Field Effect.
  50    If the virtual field velocity approaches c, the ILG kernel treats it
  51    as a relativistic mass current, even if no matter is moving. -/

depends on (8)

Lean names referenced from this declaration's body.

Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use