toInt_one
plain-language theorem explainer
The integer recovery map sends the multiplicative unit of the forced arithmetic to ordinary 1. Ring and field constructions on logic-derived integers and rationals cite this as a simp fact when discharging unit laws and denominator non-zero proofs. The argument unfolds through LogicNat.toNat, uses definitional equality, and closes by norm_num.
Claim. The recovery map from forced arithmetic to ordinary integers sends the unit to one: if $1$ denotes the multiplicative identity in the forced structure, then its image is the integer $1$.
background
LogicNat is the inductive type forced by the Law of Logic: identity is the zero-cost (multiplicative) base of the orbit, and step adds one generator iteration, mirroring ${1,\gamma,\gamma^2,\ldots}$. The forward map toNat reads the iteration count: identity maps to $0$, and each step increments.
Integers are recovered from signed pairs (or quotients) of such orbit counts. The recovery map toInt sends a forced integer to an ordinary Int, typically by casting the positive and negative orbit lengths and subtracting. In the non-negative unit case the negative part vanishes, so toInt 1 reduces to the cast of toNat 1.
This module sits in UniversalForcing.ForcedIntegers, importing the forced semiring layer and bridging ArithmeticFromLogic / IntegersFromLogic into the T-minus-1 through T8 forcing chain.
proof idea
Term/tactic hybrid. First change the goal to the unfolded form ((LogicNat.toNat 1 : \mathbb{N}) : \mathbb{Z}) = 1. Rewrite with the definitional fact LogicNat.toNat 1 = 1 (proved by rfl, since $1$ is one step on identity). Finish with norm_num on the integer cast. No external lemmas beyond the definitional reduction of toNat on the unit.
why it matters
Unit preservation is the base case for transporting ring structure along toInt. Downstream, one_mul' and mul_one' rewrite via eq_iff_toInt_eq, toInt_mul, and this lemma, then close by ring. The rational layer uses it twice: ofLogicInt and LogicRat.one both prove the denominator $1$ is nonzero by reducing toInt 1 = toInt 0 to 1 = 0 via this fact and toInt_zero. toRat_one likewise rewrites through toInt_one before norm_num.
In the Recognition foundation this is scaffolding for arithmetic forced from logic (orbit counts), not yet the physical constants. It supports the integer and rational stages that later feed mass ladders and the forcing chain, but does not itself invoke J-cost, $\varphi$, or T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.