mk
plain-language theorem explainer
The constructor forms an integer from any pair of naturals in the logic orbit by taking the quotient class under the setoid. Researchers extending the foundation to signed quantities and ledger events cite this when building integer expressions from positive orbits. It is implemented as a direct one-line application of the quotient constructor to the input pair.
Claim. The map sending a pair of natural numbers from the logic orbit to their equivalence class in the Grothendieck completion of the naturals under addition.
background
The natural numbers type is the inductive type generated by an identity element (zero-cost multiplicative identity) and a step constructor (one iteration of the generator), forming the smallest orbit closed under multiplication by the forcing element. The integer type is realized as the quotient of pairs of these naturals by the setoid equivalence (a, b) ~ (c, d) precisely when a + d = b + c, which is the standard Grothendieck construction that yields the integers as a group under addition. This module imports the arithmetic foundation to access the natural numbers type and supplies the basic constructor for producing signed integers from positive orbits.
proof idea
This is a one-line definition that applies Quotient.mk' directly to the pair of natural numbers using the setoid on their product.
why it matters
This constructor supplies the integers required for the algebra layer, appearing in the definition of the phi-ring integers as pairs of rational and phi parts and in the theorem establishing that paired events sum to zero under conjugation. It closes the step from natural orbits to signed quantities in the Recognition Science framework, supporting the mass formula on the phi-ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.