pith. machine review for the scientific record. sign in
def definition def or abbrev high

arithmeticOf

show as:
view Lean formalization →

The definition extracts the forced arithmetic object from any Law-of-Logic realization by pulling its internal identity-step orbit into a Peano algebra. Researchers working on universal forcing or logic realizations would cite this to establish the invariant arithmetic across different models. It is implemented as a one-line wrapper delegating to the extracted constructor in ArithmeticOf.

claimFor any realization $R$ of the Law of Logic, the forced arithmetic object $A(R)$ is the Peano algebra extracted from $R$'s orbit together with its initiality witness.

background

The UniversalForcing module states the first formal version of the Universal Forcing theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. Key upstream definitions include ArithmeticOf, the structure pairing a PeanoObject with a proof of its initiality, and LogicNat, the inductive type whose identity and step constructors generate the multiplicative orbit {1, γ, γ², …} as the smallest subset of positive reals closed under the generator and containing the zero-cost element. The extraction step uses the realization's own internal orbit rather than an external reference object.

proof idea

This is a one-line wrapper that applies ArithmeticOf.extracted to the input realization, constructing the structure with peano set to realizationPeano R and initial set to realization_initial R.

why it matters in Recognition Science

This definition supplies the central object referenced by every downstream invariant, including categorical_arithmetic_invariant, bool_arithmetic_invariant, modular_arithmetic_invariant, ordered_arithmetic_invariant, and physics_arithmetic_invariant, each of which invokes equivOfInitial to obtain the canonical equivalence between initial Peano algebras. It realizes the first theorem form of Universal Forcing and supplies the arithmetic spine used in later physics and engineering modules. In the Recognition framework it marks the transition from logic realizations to the invariant arithmetic that supports the phi-ladder and forcing chain.

scope and limits

formal statement (Lean)

  17def arithmeticOf (R : LogicRealization) : ArithmeticOf R :=

proof body

Definition body.

  18  ArithmeticOf.extracted R
  19
  20/-- **Universal Forcing, first theorem form.**
  21
  22For any two Law-of-Logic realizations, the arithmetic objects extracted from
  23them are canonically equivalent. In this first formal spine the equivalence is
  24the unique equivalence between initial Peano algebras. Later realization
  25modules enrich the interpretation map from each carrier into this invariant
  26arithmetic object. This definition now uses the realization's own internal
  27orbit, not the reference `LogicNat` object. -/

used by (32)

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

… and 2 more

depends on (19)

Lean names referenced from this declaration's body.