AssistedPrimeCoordinateTransform
plain-language theorem explainer
Packages a named external factorization oracle as a map that, for every nonzero non-unit finite distinction orbit N, returns prime-power coordinates reconstructing N. Foundation authors cite it when classical prime factorization is admitted under an explicit commitment string rather than derived inside the δ-calculus. As a structure definition it carries no proof; inhabitants supply the name and the total transform.
Claim. An assisted prime-coordinate transform is a pair $(c, T)$ where $c$ is a commitment name (string) and $T$ assigns to every finite distinction orbit $N \neq 0$ that is not the multiplicative unit a list of prime-power coordinates whose product reconstructs $N$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): zero and successor, the Peano skeleton of the δ-orbit. Multiplicative structure on these orbits has a native unit predicate: the only unit is the one-step orbit. Nonzero non-unit orbits are the candidates for nontrivial factorization.
PrimeCoordinateData N is a list of prime-power coordinates together with a reconstruction witness that their product equals N. The unassisted transform would produce such data from internal δ-structure alone. The assisted variant, documented as "a weaker transform that is allowed to rely on a named external readout," records an explicit commitment string so that classical factorization may be imported without pretending it was derived inside the orbit calculus.
Upstream, the ArithmeticFromLogic back structure witnesses that abstract Peano structure embeds as orbit structure under multiplication by a nontrivial positive real generator; the present package sits on the factorization side of that bridge, after physical period readout.
proof idea
No proof body: this is a structure definition (two fields). An inhabitant is a string commitmentName plus a total function transform with type $\forall N,, N\neq 0 \to \neg\mathrm{unit}(N) \to \mathrm{PrimeCoordinateData}, N$. Well-formedness of any concrete instance reduces to supplying that function and whatever external factorization lemma the commitment names.
why it matters
Inside Foundation.PrimitiveRecognitionCalculus.Factorization, prime-coordinate transport is the bridge from δ-orbit arithmetic to classical multiplicative form. The assisted package is the honest interface when that bridge is not yet closed internally: it forces every use of external factorization to carry a named commitment, separating scaffolding from proved internal transforms.
No downstream consumers are wired yet (used_by empty), so the declaration is infrastructure for later classical-factorization transport back into δ (the section that follows in the module). It does not itself touch T5–T8, RCL, or the mass ladder; it only disciplines how prime factorization may enter the PRC factorization layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.