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

LogicRealization

show as:
view Lean formalization →

LogicRealization supplies the minimal interface of a carrier set equipped with a comparison cost, zero element, generator step, and an orbit satisfying induction together with equivalence to LogicNat. Researchers extracting uniform arithmetic from disparate Law-of-Logic settings cite the structure when constructing ArithmeticOf objects. The declaration is a direct structure definition that assembles the listed fields and proposition carriers without further reduction steps.

claimA structure consists of a carrier type $C$, a cost type $K$ with zero, a comparison map $C×C→K$, a zero element $0∈C$, a successor $s:C→C$, an orbit type $O$ with its zero and successor, an interpretation $ι:O→C$ that preserves zero and successor, an equivalence $O≃LogicNat$ preserving zero and successor, the axioms compare$(x,x)=0$ and compare$(x,y)=$compare$(y,x)$, the existence of a nontrivial element with compare$(x,0)≠0$, and three proposition fields for excluded middle, composition, and action invariance.

background

LogicRealization provides the setting-independent interface for the Universal Forcing program. The module creates the common object into which different Law-of-Logic settings, continuous positive ratios, discrete propositions, or categorical structures, can be mapped. The invariant target is the arithmetic object extracted from the identity-step data rather than the ambient carrier.

proof idea

This declaration is a structure definition. It directly encodes the carrier, cost, zero, step, orbit, interpretation, equivalence to LogicNat, and the listed axioms and proposition fields without invoking lemmas or tactics.

why it matters in Recognition Science

LogicRealization supplies the data from which ArithmeticOf extracts the Peano object and its initiality, including the canonical and extracted variants that produce Peano surfaces. It fills the interface step in the Universal Forcing program, allowing realizations from kinship graphs, nucleosynthesis tiers, and cellular automata to feed into uniform arithmetic extraction. The structure ensures the extracted arithmetic remains independent of the specific topology or order supplied by each realization.

scope and limits

formal statement (Lean)

  32structure LogicRealization where
  33  Carrier : Type u
  34  Cost : Type v
  35  zeroCost : Zero Cost
  36  compare : Carrier → Carrier → Cost
  37  zero : Carrier
  38  step : Carrier → Carrier
  39  Orbit : Type u
  40  orbitZero : Orbit
  41  orbitStep : Orbit → Orbit
  42  interpret : Orbit → Carrier
  43  interpret_zero : interpret orbitZero = zero
  44  interpret_step : ∀ n : Orbit, interpret (orbitStep n) = step (interpret n)
  45  orbit_no_confusion : ∀ n : Orbit, orbitZero ≠ orbitStep n
  46  orbit_step_injective : Function.Injective orbitStep
  47  orbit_induction :
  48    ∀ P : Orbit → Prop,
  49      P orbitZero →
  50      (∀ n, P n → P (orbitStep n)) →
  51      ∀ n, P n
  52  orbitEquivLogicNat : Orbit ≃ LogicNat
  53  orbitEquiv_zero : orbitEquivLogicNat orbitZero = LogicNat.zero
  54  orbitEquiv_step : ∀ n : Orbit,
  55    orbitEquivLogicNat (orbitStep n) = LogicNat.succ (orbitEquivLogicNat n)
  56  identity : ∀ x : Carrier, compare x x = 0
  57  nonContradiction : ∀ x y : Carrier, compare x y = compare y x
  58  excludedMiddle : Prop
  59  composition : Prop
  60  actionInvariant : Prop
  61  nontrivial : ∃ x : Carrier, compare x zero ≠ 0
  62
  63attribute [instance] LogicRealization.zeroCost
  64
  65namespace LogicRealization
  66
  67/-- The identity-step shadow of a realization. This is the data from which
  68`ArithmeticOf` extracts arithmetic. -/

used by (40)

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

… and 10 more

depends on (22)

Lean names referenced from this declaration's body.