Supporting results for pointwise provable equality.

Classification of the generated composition congruence.

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.generated_iff_extensional_of_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : SigmaOneSound T) (F G : ProofSearch.FunctionalGraph) : Rel T F G ↔ PiOneCharacterization.Extensional ↑F ↑G

In the Sigma-one sound case the generated congruence is exactly extensional equality. The containment hypothesis is fully discharged.

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.generated_universal_of_not_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : ¬SigmaOneSound T) (F G : ProofSearch.FunctionalGraph) : Rel T F G

Failure of Sigma-one soundness makes every two functional graphs equivalent in the generated congruence.

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.classification (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : (SigmaOneSound T → ∀ (F G : ProofSearch.FunctionalGraph), Rel T F G ↔ PiOneCharacterization.Extensional ↑F ↑G) ∧ (¬SigmaOneSound T → ∀ (F G : ProofSearch.FunctionalGraph), Rel T F G)

The generated-congruence dichotomy, with no consistency or effective presentation assumption on T.

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.generated_iff_extensional_or_unsound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F G : ProofSearch.FunctionalGraph) : Rel T F G ↔ PiOneCharacterization.Extensional ↑F ↑G ∨ ¬SigmaOneSound T

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.quotient_subsingleton_of_not_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : ¬SigmaOneSound T) : Subsingleton (QuotientGraph T)

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.quotient_subsingleton_iff_not_sound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] : Subsingleton (QuotientGraph T) ↔ ¬SigmaOneSound T

The quotient monoid has one element exactly in the unsound case.