Supporting results for pointwise provable equality.
An independent productive-set proof of the range-assignment obstruction. The probe tests whether the concrete diagonal history has a positive result at the supplied stage. Every standard stage is separately PA-refutable, while the internally quantified absence sentence is unprovable in the ambient theory.
True diagonal divergence refutes the positive-history test at each standard stage.
Absence of all positive history stages is exactly diagonal divergence in PA.
A concrete productive divergence witness gives the required range counterexample.
Productiveness supplies the witness for an enumerable theorem-code set.
The productive proof requires only recursively enumerable axiom codes.
The explicit program-enumerator specialization of the productive route.
The same productive witness rules out an induced operation on the quotient.