current_residual_named
plain-language theorem explainer
The residual currently tracked by the factorization goal-closure layer is exactly the prime-coordinate readout residual. Anyone assembling the GoalClosureCertificate cites this equality to pin the residual name. The proof is pure reflexivity against the definition of the current residual.
Claim. The residual name presently retained for historical compatibility equals the prime-coordinate readout residual (the original D4 commitment that supplies the $\delta$-prime-coordinate transform).
background
In the Primitive Recognition Calculus factorization layer, residual names label which open commitment the goal-closure machinery is still tracking. The enum value for the prime-coordinate readout residual is the original D4 commitment: supplying it means supplying the $\delta$-prime-coordinate transform itself, not a weaker benchmark.
The definition currentPrimeCoordinateResidual hard-wires that residual as the active label "retained for historical compatibility," with the commitment closed below by the native-choice transform. This module packages those facts into a single certificate structure once the transform provenance and exactness lemmas are in place.
proof idea
One-line reflexivity. Unfolding the definition of the current residual yields the constructor .primeCoordinateReadout on the nose, so rfl closes the equality.
why it matters
This pin is the first field of goal_closure_certificate, which bundles residual naming, transform provenance, exactness, closure, and prime-divisor recovery into one GoalClosureCertificate record. Without a named residual equal to the prime-coordinate readout, the certificate cannot assert that the D4 commitment is the one being closed. It is bookkeeping rather than physics, but it locks the historical residual label to the transform that the rest of the factorization closure actually discharges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.