Borisov's converse from the published normal-form inputs

This file is the assembly point for the converse direction of Borisov's criterion. The presentation-level Assertions IV--V and the coefficient classification in Assertion V supply every input used by the iterated-HNN proof.

theorem Undecidability.BorisovConverseClassified.criterion_converse_of_classification (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BorisovContextNormalForm.BaseIntersections datum) (hclass : BorisovLemma4Pinch.PinchClassification datum hfree) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) → ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

The converse simulation theorem with the required Gamma3 normal-form inputs displayed explicitly. All c, t, and k HNN stages, the ordered double-coset extraction, and the full Lemma-4 induction are discharged.

theorem Undecidability.BorisovConditionalConverse.criterion_converse_of_shapes (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BorisovContextNormalForm.BaseIntersections datum) (hsource : ∀ (Q : List (Fin 2)) (f r : ℤ), BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum → BorisovPinchCoefficientClassification.SourceCoefficientShape datum Q f r) (htarget : ∀ (Q : List (Fin 2)) (f r : ℤ), BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum → BorisovPinchCoefficientClassification.TargetCoefficientShape datum Q f r) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) → ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

Minimal semantic boundary for the converse: rank-five freeness, the two base intersections, and the literal coefficient shapes.

theorem Undecidability.BorisovConditionalConverse.criterion_converse_of_positive_sparse_parsers (datum : Thue.StandingDatum) (hsourcePositive : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCStage.RuleBasis), (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → BorisovCoefficientShapes.AllPositive w.toWord) (hsourceSparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCStage.RuleBasis), (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → BorisovCoefficientShapes.ruleCount w.toWord ≤ 1) (htargetPositive : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCStage.RuleBasis), (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → BorisovCoefficientShapes.AllPositive w.toWord) (htargetSparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCStage.RuleBasis), (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → BorisovCoefficientShapes.ruleCount w.toWord ≤ 1) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) → ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

Parser-facing form of criterion_converse_of_shapes: positivity and the absence of two displayed rule letters are the exact two facts consumed from the coefficient-by-coefficient comparison of flat HNN normal forms.

theorem Undecidability.BorisovConditionalConverse.criterion_converse_of_sparse_parsers (datum : Thue.StandingDatum) (hsourceSparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCStage.RuleBasis), (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → BorisovCoefficientShapes.ruleCount w.toWord ≤ 1) (htargetSparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCStage.RuleBasis), (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → BorisovCoefficientShapes.ruleCount w.toWord ≤ 1) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) → ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

Flat-signature uniqueness supplies positivity automatically. Thus the page-771 parser input used here is that a canonical rank-five preimage contains at most one displayed rule letter.