_ordered_ok
This definition records that the Peano carrier extracted from the arithmetic of the strict ordered integer realization is canonically equivalent to the logic-forced natural numbers. Researchers auditing the strict completion of Universal Forcing cite it to confirm that the ordered model yields the expected arithmetic orbit. The proof is a one-line wrapper that invokes the orbit equivalence supplied by the lightweight conversion of the realization.
claimThe carrier of the Peano arithmetic derived from the strict ordered integer realization is equivalent to the inductive type of logic-forced natural numbers (identity element plus successor steps).
background
The module supplies an audit surface for the strict, domain-rich Universal Forcing completion pass. A StrictLogicRealization consists of a carrier type, a cost type equipped with zero, a comparison map, and a composition operation; the strictOrderedRealization instantiates this with integer carrier and natural-number costs. The arith operation extracts the forced arithmetic from the lightweight version of any such realization, while LogicNat is the inductive type whose identity constructor represents the zero-cost element and whose step constructor iterates the generator, mirroring the orbit closed under multiplication by the generator and containing the multiplicative identity.
proof idea
One-line wrapper that applies the orbit equivalence from the lightweight realization of the strict ordered model.
why it matters in Recognition Science
The definition belongs to the AxiomAudit module that verifies the strict completion pass. It confirms that the ordered integer model produces the logic-forced naturals required by the Law of Logic, thereby supporting the derivation of arithmetic inside the forcing chain. No downstream uses are recorded, indicating its role as an internal consistency check rather than a lemma invoked elsewhere.
scope and limits
- Does not establish equivalence for non-ordered or non-strict realizations.
- Does not derive physical constants or mass formulas.
- Does not address continuous or non-discrete models.
formal statement (Lean)
51def _ordered_ok :
52 (StrictLogicRealization.arith strictOrderedRealization).peano.carrier
53 ≃ ArithmeticFromLogic.LogicNat :=
proof body
Definition body.
54 (StrictLogicRealization.toLightweight strictOrderedRealization).orbitEquivLogicNat
55