Supporting results for pointwise provable equality.

Elementary composition laws for the Pi-one completeness characterization. The input quantifier in pointwise provability remains external throughout.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.pointwise_comp_left (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F G H : ProofSearch.Graph) (hGH : ProofSearch.Pointwise T G H) : ProofSearch.Pointwise T (ProofSearch.comp F G) (ProofSearch.comp F H)

Composing on the left by a fixed graph always preserves pointwise provability. The quantified intermediate value remains inside each proof.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.extensional_comp {F F' G G' : ProofSearch.Graph} (hF : Extensional F F') (hG : Extensional G G') : Extensional (ProofSearch.comp F G) (ProofSearch.comp F' G')

Standard equality of graph extensions is preserved in both arguments of composition, without a functionality hypothesis.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.congruence_iff_rightCompatible (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : CompositionCongruence T ↔ RightCompatible T

The other variable of composition is automatically compatible, so full congruence is equivalent to compatibility under right composition.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.rightCompatible_of_pointwise_iff_extensional (T : FFL.FirstOrder.ArithmeticTheory) (h : AgreesWithExtensional T) : RightCompatible T

Agreement between pointwise provability and standard graph equality on functional graphs suffices for compatibility under right composition.

theorem PointwiseComposition.FailureOfComposition.PiOneCharacterization.compositionCongruence_of_pointwise_iff_extensional (T : FFL.FirstOrder.ArithmeticTheory) (h : AgreesWithExtensional T) : CompositionCongruence T

The same agreement gives full compatibility with composition.