currentPrimeCoordinateResidual
plain-language theorem explainer
Pins the active D4 residual label to prime-coordinate readout, kept for historical naming of the factorization finish line. Anyone citing the goal-closure certificate or residual-name equality will use this constant. The body is a one-constructor assignment of the residual-name inductive.
Claim. The residual name currently selected at the D4 finish line is the prime-coordinate readout residual (among the allowed labels: prime-coordinate readout, character-spectrum readout, physical-period readout, and classical factorization transport).
background
In the Primitive Recognition Calculus factorization track, D4 is the finish line for recovering prime coordinates of a positive integer from a $\delta$-display. Residuals at that line are named by a small inductive type whose constructors mark which readout or transport path is claimed: prime-coordinate readout, character-spectrum readout, physical-period readout, or classical factorization transport.
The module keeps a single "current" residual label so downstream certificates can name one commitment without hard-coding constructors everywhere. Upstream, a classical-transport transform already exists: Mathlib's Nat.primeFactorsList is carried through the established $\delta$/Nat display equivalence, closing a theorem-level $\delta$ prime-coordinate transform without claiming a new fast factoring algorithm.
Local setting is goal closure for that D4 commitment: the residual label and the transform provenance together form the certificate that factor recovery is closed by a native noncomputable $\delta$-choice path, with classical transport recorded separately.
proof idea
Definitional one-liner. The value is the inductive constructor for prime-coordinate readout; no tactics or lemmas are applied. Equality to that constructor is then immediate by rfl in the sibling naming theorem.
why it matters
This constant is the residual half of the D4 closure certificate. That certificate requires both that the current residual equals prime-coordinate readout and that transform provenance is native $\delta$ readout; classical transport remains a separate proved path. The sibling theorem current_residual_named is just reflexivity on this definition, so every consumer of the certificate depends on this pin.
In the broader Recognition factorization story it records which finish-line residual is live after the native-choice transform closed the original D4 commitment. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is bookkeeping that keeps the goal-closure Prop honest about which residual was discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.