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)
29def boolOrbitInterpret : ArithmeticFromLogic.LogicNat → Bool
30 | ArithmeticFromLogic.LogicNat.identity => false
31 | ArithmeticFromLogic.LogicNat.step n => Bool.not (boolOrbitInterpret n)
32
33/-- The discrete propositional Law-of-Logic realization. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
boolRealization
in IndisputableMonolith.Foundation.DiscreteLogicRealization
decl_use
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use