`continuous_positive_ratio_arithmetic_invariant`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing
domain: Foundation
line: 50 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  47
  48/-- The continuous positive-ratio realization has the same forced arithmetic
  49as every other realization. -/
  50noncomputable def continuous_positive_ratio_arithmetic_invariant
  51    (C : LogicAsFunctionalEquation.ComparisonOperator)
  52    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
  53    (S : LogicRealization.{0, 0}) :
  54    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
  55      ≃ (arithmeticOf S).peano.carrier :=
  56  ArithmeticOf.equivOfInitial
  57    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)) (arithmeticOf S)
  58
  59/-- The Peano surface is available for the forced arithmetic of every
  60realization. -/
  61theorem peano_surface (R : LogicRealization) :
  62    ArithmeticOf.PeanoSurface (arithmeticOf R) :=
  63  ArithmeticOf.extracted_peanoSurface R
  64
  65end UniversalForcing
  66end Foundation
  67end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.