toIntCore
plain-language theorem explainer
toIntCore converts each pair of logic naturals into an integer by subtracting the iteration counts of the two components. It is the raw difference function later lifted to the quotient in the integers-from-logic construction. The definition is a direct lambda that applies the iteration-count map to each entry and subtracts after casting to Int.
Claim. The function sending a pair of logic naturals $(a,b)$ to the integer obtained by subtracting the natural-number value of $b$ from that of $a$, where the natural-number value is the iteration count that sends the base element to zero and each successor step to the next natural number.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost base element) and step (one iteration of the generator), representing the smallest orbit closed under the forced multiplication. The map toNat extracts the iteration count by sending identity to zero and recursing with successor on each step. This definition lives in the integers-from-logic module, which imports the arithmetic-from-logic layer to prepare pairs for quotienting.
proof idea
One-line definition that applies toNat to each component of the input pair, casts both results to Int, and subtracts them.
why it matters
It supplies the concrete difference map that toInt lifts via Quotient.lift and that toIntCore_respects proves invariant under the pair equivalence. The declaration therefore completes the raw arithmetic embedding of logic naturals into standard integers inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.