sound
plain-language theorem explainer
The sound theorem asserts that the mk constructor for LogicInt is invariant under the defining relation of the quotient: whenever a + d equals c + b in LogicNat, the pairs represent the same integer. Foundational work on constructing integers from the forced naturals in Recognition Science cites this to ensure well-defined arithmetic. The proof is a direct one-line application of Quotient.sound to the supplied equality.
Claim. Let $a,b,c,d$ belong to LogicNat. If $a + d = c + b$, then $[a, b]_ℓ = [c, d]_ℓ$ in the Grothendieck group LogicInt.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, representing the orbit under multiplication by the generator in the positive reals. LogicInt is the quotient of LogicNat × LogicNat by the setoid whose relation is (a, b) ~ (c, d) precisely when a + d = c + b; mk forms the class [a, b]_ℓ that stands for the formal difference a − b. This declaration belongs to the module that embeds LogicNat into its Grothendieck completion, supplying the integers required for subsequent arithmetic definitions.
proof idea
The proof is a one-line wrapper that applies Quotient.sound directly to the hypothesis h : a + d = c + b, which shows the two pairs are related by the setoid and therefore have identical quotient classes.
why it matters
The result guarantees that mk is well-defined on equivalence classes, which is required before addition and multiplication on LogicInt can be lifted via Quotient.lift₂. It feeds the add, mul, and fromInt_toInt declarations in the same module and supports downstream uses such as BWD3Model in complexity and virtue signatures in ethics. Within the Recognition framework it completes the passage from LogicNat to LogicInt, enabling the integer arithmetic presupposed by the forcing chain and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.