def definition def or abbrev

`strictBoolean_arith_equiv_logicNat`

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

formal statement (Lean)

  53def strictBoolean_arith_equiv_logicNat :
  54    (StrictLogicRealization.arith strictBooleanRealization).peano.carrier
  55      ≃ ArithmeticFromLogic.LogicNat :=

proof body

Definition body.

  56  (StrictLogicRealization.toLightweight strictBooleanRealization).orbitEquivLogicNat
  57
  58/-- First strict cross-realization invariance theorem:
  59positive ratios and Boolean propositions force the same arithmetic. -/

depends on (8)

Lean names referenced from this declaration's body.

carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
strictBooleanRealization in IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean decl_use
arith in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
toLightweight in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use