currentPrimeCoordinateTransformProvenance
plain-language theorem explainer
Tags the currently closed prime-coordinate transform as native δ-readout (prime/factorization descent), not classical factorization transport. Cited by the D4 goal-closure certificate and the reflexivity theorem that pins this choice. One-constructor definition selecting that provenance branch.
Claim. The active provenance of the closed prime-coordinate transform is the native $\delta$-readout path obtained by prime/factorization descent (as opposed to classical factorization transport).
background
In the factorization goal-closure layer, a transform that recovers prime factors may be closed along either of two routes. The inductive type of transform provenance records which route is currently closed: classical factorization transport, or native $\delta$-readout.
Native readout chooses a noncomputable $\delta$ by prime/factorization descent so that factor recovery becomes coordinate readout on the residual. The surrounding module packages a D4 closure certificate around that choice, keeping classical transport as a separate proved path.
proof idea
One-line definition: inhabit the provenance type by the nativeDeltaReadout constructor. No lemmas, no tactics, no obligations beyond type-checking the constructor.
why it matters
Supplies the provenance field of the D4 goal-closure certificate, which records that factor recovery is closed by a native noncomputable $\delta$-choice transform while classical transport stays a separate proved path. Also feeds the reflexivity theorem asserting that the current provenance equals native $\delta$-readout. Together with the residual-naming commitment, this is the bookkeeping that makes "solving becomes coordinate readout" a certificate rather than a slogan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.