def definition def or abbrev

`boolean_freeOrbit_isNNO`

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

formal statement (Lean)

 291def boolean_freeOrbit_isNNO :
 292    IsNaturalNumberObject
 293      (N := StrictLogicRealization.FreeOrbit strictBooleanRealization)

proof body

Definition body.

 294      LogicNat.identity LogicNat.step :=
 295  logicNat_isNNO
 296
 297end Strict.DiscreteBoolean
 298
 299end UniversalForcing
 300end Foundation
 301end IndisputableMonolith

depends on (9)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
IsNaturalNumberObject in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
logicNat_isNNO in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
strictBooleanRealization in IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean decl_use
FreeOrbit in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use