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)
67theorem bool_hasIdentityStep : boolRealization.hasIdentityStep :=
proof body
Term-mode proof.
68 LogicRealization.hasIdentityStep_of_nontrivial boolRealization
69
70/-- Boolean realization has the same forced arithmetic as every realization. -/
depends on (6)
Lean names referenced from this declaration's body.
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
boolRealization
in IndisputableMonolith.Foundation.DiscreteLogicRealization
decl_use
-
hasIdentityStep
in IndisputableMonolith.Foundation.LogicRealization
decl_use
-
hasIdentityStep_of_nontrivial
in IndisputableMonolith.Foundation.LogicRealization
decl_use
-
LogicRealization
in IndisputableMonolith.Foundation.LogicRealization
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use