FactorPair
plain-language theorem explainer
A factor pair packages two orbit positions whose product recovers a given orbit position n, with the equality held as a field. Anyone working on chart transitions or magnitude underdetermination in the primitive recognition calculus cites it. As a structure definition there is no proof body; the content is the three fields left, right, and product equality.
Claim. For an orbit position $n$ in the base-neutral distinction naturals, a factor pair is a triple $(L,R,p)$ where $L$ and $R$ are distinction naturals and $p$ is a proof that $L \cdot R = n$.
background
Distinction naturals are the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, carrying a native multiplication. They stand in for ordinary natural numbers when the calculus must stay free of a preferred radix.
This module sits in the factorization layer of the primitive recognition calculus. The surrounding siblings treat the product as what a positional chart can see, and study when the same product arises from distinct left or right factors (e.g. $2\cdot 6 = 3\cdot 4$). A factor pair is the native witness that two orbit positions multiply to a target $n$.
The structure is the data type those later lemmas quantify over: left factor, right factor, and the equality certificate.
proof idea
No proof. The declaration is a structure (record type) with three fields: left and right of type DistinctionNat, and product_eq asserting left * right = n. Inhabitation is by providing concrete factors and a multiplicative equality proof in DistinctionNat.
why it matters
Chart-transition and magnitude arguments in this module need a first-class object for "two factors whose product is n". Factor pairs supply that object so later results can state that the positional chart sees only the product, that equal products share archimedean magnitude, and that magnitude underdetermines each factor separately (siblings such as same_product_same_magnitude and magnitude_underdetermines_left_factor).
In the Recognition foundation this is bookkeeping for orbit factorization before geometric or physical layers attach. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder; it only equips the distinction-orbit arithmetic those layers will use when factorization of orbit positions matters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.