Supporting results for pointwise provable equality.

The stage-restricted witnesses are pointwise PA-equivalent whenever the underlying graphs agree on the standard naturals. A true ground equation for the total history evaluator fixes all possible internal outputs at that standard stage and input. No uniform equivalence premise is assumed.

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.AGraph_eqAt_B_pair (e : ℕ) (G : ProofSearch.Graph) (hExt : PiOneCharacterization.Extensional (ConcreteEvaluator.eventualGraph e) G) (s x : ℕ) : 𝐏𝐀 ⊢ ProofSearch.eqAt (AGraph e G) (BGraph e) (Nat.pair s x)

At each fixed standard stage/input pair, PA proves equality of the two witness graphs over all internal outputs.

theorem PointwiseComposition.FailureOfComposition.GeneratedWitnessGraphs.AGraph_pointwise_B (e : ℕ) (G : ProofSearch.Graph) (hExt : PiOneCharacterization.Extensional (ConcreteEvaluator.eventualGraph e) G) : ProofSearch.Pointwise 𝐏𝐀 (AGraph e G) (BGraph e)

Standard equality of the original graphs suffices for pointwise PA-provable equality of the stage-restricted witnesses. No functionality assumption on G and no uniform-equivalence premise is needed.