Positivity in Borisov's coefficient normal form

The full flat-signature uniqueness theorem compares the literal expansion of a rank-five word with the positive flat representative of d^f Q e^r. Consequently every displayed rank-five letter has positive sign. This is the positivity half of Borisov's page-771 coefficient parser.

@[reducible, inline]

abbrev Undecidability.BorisovCoefficientSignComparison.FlatWord : Type

A reduced word in the flattened two-stable-letter HNN model.

Equations

• Undecidability.BorisovCoefficientSignComparison.FlatWord = Undecidability.MultipleHNNFlat.ReducedWord Undecidability.BorisovHNNModel.A0 Undecidability.BorisovHNNModel.B0

def Undecidability.BorisovCoefficientSignComparison.positiveCoefficientWord (Q : List (Fin 2)) (f r : ℤ) : FlatWord

The literal flat reduced word for d^f Q e^r, where Q is a positive word in the two stable letters.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Undecidability.BorisovCoefficientSignComparison.positiveCoefficientWord_signature (Q : List (Fin 2)) (f r : ℤ) : MultipleHNNFlat.signature BorisovHNNModel.A0 BorisovHNNModel.B0 (positiveCoefficientWord Q f r) = List.map (fun (beta : Fin 2) => (beta, 1)) Q

theorem Undecidability.BorisovCoefficientSignComparison.positiveCoefficientWord_eval (Q : List (Fin 2)) (f r : ℤ) : MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (positiveCoefficientWord Q f r) = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r

Positivity extracted from signature equality

theorem Undecidability.BorisovCoefficientSignComparison.allPositive_iff_forall_sign (letters : List (BorisovCoefficientShapes.Basis × Bool)) : BorisovCoefficientShapes.AllPositive letters ↔ ∀ x ∈ letters, x.2 = true

theorem Undecidability.BorisovCoefficientSignComparison.factorRun_has_own_sign (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovCoefficientShapes.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : ∃ s ∈ BorisovAssertionIV.factorRun rules hne x lastCoeff, s.sign = BorisovAssertionIV.signedUnit x.2

theorem Undecidability.BorisovCoefficientSignComparison.expansionTail_has_factor_sign (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovCoefficientShapes.Basis × Bool)) (x : BorisovCoefficientShapes.Basis × Bool) (hx : x ∈ letters) : ∃ s ∈ BorisovAssertionIV.expansionTail rules hne letters, s.sign = BorisovAssertionIV.signedUnit x.2

theorem Undecidability.BorisovCoefficientSignComparison.allPositive_of_expansion_signature (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovCoefficientShapes.Basis × Bool)) (hreduced : List.IsChain (fun (x y : BorisovCoefficientShapes.Basis × Bool) => x.1 = y.1 → x.2 = y.2) letters) (Q : List (Fin 2)) (hsignature : MultipleHNNFlat.signature BorisovHNNModel.A0 BorisovHNNModel.B0 (BorisovAssertionIV.expansionWord rules hne letters hreduced) = List.map (fun (beta : Fin 2) => (beta, 1)) Q) : BorisovCoefficientShapes.AllPositive letters

If a literal rank-five expansion has the same signature as a positive stable word, every displayed rank-five letter is positive.

theorem Undecidability.BorisovCoefficientSignComparison.u_allPositive_of_coefficient_eq (datum : Thue.StandingDatum) (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCoefficientShapes.Basis) (heval : (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r) : BorisovCoefficientShapes.AllPositive w.toWord

Signature comparison supplies the complete positivity half of Borisov's page-771 coefficient parser for the source basis.

theorem Undecidability.BorisovCoefficientSignComparison.v_allPositive_of_coefficient_eq (datum : Thue.StandingDatum) (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup BorisovCoefficientShapes.Basis) (heval : (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r) : BorisovCoefficientShapes.AllPositive w.toWord

Target-basis counterpart of u_allPositive_of_coefficient_eq.