def definition def or abbrev

`deltaOf`

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

formal statement (Lean)

  16@[simp] def deltaOf (gen : Ribbons.GenClass) (p : Primitive) : ℤ :=

proof body

Definition body.

  17  Ribbons.rungFrom gen p.word
  18
  19-- deltaOf is definitionally invariant (tautological; placeholder for rung-independence proof)
  20example (p : Primitive) (gen : Ribbons.GenClass) : deltaOf gen p = deltaOf gen p := rfl
  21
  22end SectorPrimitive
  23end Masses
  24end IndisputableMonolith

depends on (14)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
Primitive in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
GenClass in IndisputableMonolith.Masses.KernelTypes decl_use
rungFrom in IndisputableMonolith.Masses.Ribbons decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Primitive in IndisputableMonolith.Masses.SectorPrimitive decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use