strictOrderedRealization
The definition supplies a concrete strict ordered realization of logic on the integers as carrier with equality-based cost. Axiom audits and arithmetic-to-logic equivalence maps cite this model to instantiate the abstract structure. It is assembled by direct record construction that assigns the integer cost function to the compare field and invokes its reflexivity and symmetry lemmas for the required laws.
claimThe strict ordered realization is the structure with carrier set $ℤ$, cost function $c(a,b)=0$ if $a=b$ else $1$, composition given by addition on $ℤ$, identity element $0$, and generator $1$, where the identity law holds by reflexivity of the cost, the non-contradiction law by symmetry of the cost, and the excluded-middle, composition, and invariance laws hold trivially.
background
The module defines strict ordered realizations. The local setting is a strict ordered realization on $ℤ$ with equality cost and unit translation, providing a concrete model for the abstract StrictLogicRealization structure. The key auxiliary definition is the integer cost function, which assigns cost zero to equal integers and one otherwise. Upstream results establish that this cost is reflexive via intCost_self and symmetric via intCost_symm.
proof idea
The definition is a direct record construction that populates the StrictLogicRealization fields: carrier to $ℤ$, compare to the integer equality cost, compose to addition, one to $0$, generator to $1$, identity_law to intCost_self, non_contradiction_law to intCost_symm, and the remaining laws to True. The nontrivial_law is discharged by a one-line simp tactic using the cost definition.
why it matters in Recognition Science
This supplies the concrete ordered model that feeds into the axiom audit _ordered_ok and the equivalence strictOrdered_arith_equiv_logicNat. It instantiates the strict case within the universal forcing framework, connecting the integer carrier to LogicNat via the lightweight conversion. It fills the concrete instantiation step in the foundation layer.
scope and limits
- Does not establish uniqueness of this realization among possible carriers.
- Does not derive the forcing chain steps T5-T8 or the Recognition Composition Law.
- Does not connect to physical constants such as alpha or G.
- Does not handle non-strict or non-ordered variants of the realization.
Lean usage
(StrictLogicRealization.toLightweight strictOrderedRealization).orbitEquivLogicNatformal statement (Lean)
29def strictOrderedRealization : StrictLogicRealization where
30 Carrier := ℤ
proof body
Definition body.
31 Cost := Nat
32 zeroCost := inferInstance
33 compare := intCost
34 compose := fun a b => a + b
35 one := 0
36 generator := 1
37 identity_law := intCost_self
38 non_contradiction_law := intCost_symm
39 excluded_middle_law := True
40 composition_law := True
41 invariance_law := True
42 nontrivial_law := by
43 simp [intCost]
44