one_toInt
plain-language theorem explainer
The multiplicative unit among signed δ-orbits recovers to the ordinary integer 1 under the PRC integer map. Anyone proving unit laws, divisibility, or reciprocal identities in the primitive recognition calculus cites this simp fact. The proof is pure definitional equality (rfl).
Claim. If $\mathbf{1}$ denotes the multiplicative unit signed orbit, then its integer recovery satisfies $\mathrm{toInt}(\mathbf{1}) = 1$.
background
In the Primitive Recognition Calculus, integers are realized as signed δ-orbits: pairs of nonnegative orbit positions (positive and negative legs) quotiented by the balance relation $a.pos + b.neg = b.pos + a.neg$. The map toInt sends a signed orbit to an ordinary Int by recovering the net length of those legs; it is the PRC-side analogue of the LogicInt recovery map.
The constant one is the multiplicative unit in this monoid of signed orbits. The sibling fact zero_toInt records the additive identity case. The local setting is the IntegerRational layer, which builds rationals from these signed orbits before real completion.
proof idea
One-line rfl. By construction of the unit signed orbit and of toInt, both sides reduce to the numeral 1, so the equality is definitional. Marked @[simp] for automatic rewriting.
why it matters
This is the unit-normalization lemma for PRC integers. Downstream it discharges the unit factor in divisibility: dvdZ_refl and one_dvdZ both rewrite mul_toInt against one_toInt then close by omega. The same rewrite appears in reciprocal cross-equality (mul_recipNonzero_crossEq_one, recipNonzero_mul_crossEq_one), in the proof that the unit is nonzero (not_isZero_one), and as the private bridge one_num_toInt for ratio-orbit units feeding PRCUnitFraction_toRat.
In the broader foundation it anchors the integer layer that sits under the forcing chain’s discrete arithmetic (eight-tick octave, rung arithmetic on the φ-ladder), without itself invoking J-cost or T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.