abbrev definition def or abbrev

`FreeOrbit`

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

formal statement (Lean)

  46abbrev FreeOrbit (_R : StrictLogicRealization) : Type :=

proof body

Definition body.

  47  LogicNat
  48
  49/-- Interpret the free orbit of a strict realization in its carrier by
  50primitive recursion over the native generator and composition operation. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

boolean_freeOrbit_isNNO in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
interpret in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
interpret_step in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
toLightweight in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use