PrimeCoordinateTransformProvenance
plain-language theorem explainer
Finite enumeration of the two allowed provenances for the closed prime-coordinate transform: classical factorization transport, or native δ readout. Goal-closure code cites it to pin the live choice. Pure inductive type with decidable equality; no proof obligations.
Claim. There are exactly two labeled sources for the closed prime-coordinate transform: classical factorization transport, and native $\delta$ readout. The object is a two-constructor enumeration equipped with decidable equality and a printable representation.
background
In the factorization goal-closure layer of the primitive recognition calculus, the prime-coordinate transform is treated as already closed, but the ledger still records how that closure was obtained. The two routes are classical transport of a factorization identity, versus a native $\delta$ readout driven by prime/factorization descent.
The native route is the one currently selected downstream. Its geometric prior is the diamond descent lemma: from any off-centre vertex there is a 4-neighbour edge to a strictly lower cell, by stepping the larger-magnitude coordinate one unit toward the origin. That height-reducing step is the combinatorial content behind "native $\delta$ choice by prime/factorization descent."
This declaration only names the provenance tags; it does not build the transform or the residual.
proof idea
No proof. The declaration is an inductive type with two nullary constructors, deriving DecidableEq and Repr. Downstream code simply inhabits one constructor (the native $\delta$ readout tag) as the current provenance value.
why it matters
Goal-closure bookkeeping needs an explicit, matchable tag for which transform story is live. The sole direct consumer is the current-provenance definition, which fixes the native $\delta$ readout constructor. That pin feeds residual naming, readout-commitment lemmas, and the goal-closure certificate in the same module: without a closed provenance tag, the certificate cannot state that the prime-coordinate readout recovers the prime divisor under the committed route.
In the broader Recognition stack this is scaffolding hygiene rather than a forcing-chain step (T5–T8). It keeps classical transport available as a named alternative while the active path is the descent-driven native readout, so later audits can see which story closed the transform.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.