arith — Recognition explainer

formal statement (Lean)

  95def arith (R : StrictLogicRealization) : ArithmeticOf (toLightweight R) :=

proof body

Definition body.

  96  arithmeticOf (toLightweight R)
  97
  98/-- Every strict realization has forced arithmetic canonically equivalent to
  99`LogicNat`. -/

used by (29)

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

_biology_ok in IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit decl_use
_categorical_ok in IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit decl_use
_ethics_ok in IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit decl_use
_music_ok in IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit decl_use
_narrative_ok in IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit decl_use
_ordered_ok in IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit decl_use
biology_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Biology decl_use
strictCategorical_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Categorical decl_use
strictBoolean_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean decl_use
strictPositiveRatio_arith_equiv_strictBoolean in IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean decl_use
ethics_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Ethics decl_use
strict_arith_universal_initial in IndisputableMonolith.Foundation.UniversalForcing.Strict.Invariance decl_use
strict_peano_surface in IndisputableMonolith.Foundation.UniversalForcing.Strict.Invariance decl_use
strict_universal_forcing in IndisputableMonolith.Foundation.UniversalForcing.Strict.Invariance decl_use
StrictMetaphysicalGround in IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical decl_use
strict_metaphysical_ground_unique in IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical decl_use
strictUniversalGround in IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical decl_use
strictModular_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular decl_use
music_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
narrative_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Narrative decl_use
strictOrdered_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered decl_use
positiveRatio_arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.Strict.PositiveRatio decl_use
positiveRatio_strict_equiv_existing in IndisputableMonolith.Foundation.UniversalForcing.Strict.PositiveRatio decl_use
arith_equiv_logicNat in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
universal_forcing in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
metaphysical_ground_invariant in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts decl_use
ArithmeticDeformationIdentification in IndisputableMonolith.NumberTheory.RiemannHypothesis.PrimeTailBounds decl_use
attachmentWithMargin_of_bossLemma in IndisputableMonolith.NumberTheory.RiemannHypothesis.PrimeTailBounds decl_use

depends on (6)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
ArithmeticOf in IndisputableMonolith.Foundation.ArithmeticOf decl_use
arithmeticOf in IndisputableMonolith.Foundation.UniversalForcing decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
toLightweight in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use