Burmese Negation Fragment

[Mie05] [Has13b] [DH13a]

Burmese expresses standard negation with a circumfix: prefix ma- on the verb and suffix -bu replacing the TAM markers of the affirmative.

Always asymmetric (A/Cat)

Burmese negation is always asymmetric: the negative suffix -bu replaces the TAM (tense-aspect-mood) markers used in the affirmative, neutralizing TAM distinctions. This is paradigmatic asymmetry: the negative paradigm has fewer formal distinctions than the affirmative.

Paradigm (sa 'eat')

Construction	Affirmative	Negative
Realis	sa-deh	ma-sa-bu
Irrealis	sa-meh	ma-sa-bu
Future	sa-laimeh	ma-sa-bu

The affirmative distinguishes realis (-deh), irrealis (-meh), and future (-laimeh), but the negative collapses all three to ma-...-bu.

def Burmese.Negation.negPrefix : String

The Burmese negative prefix. Component of the bipartite ma-...-bu circumfix; see circumfix for the substrate-typed entry.

Equations

• Burmese.Negation.negPrefix = "ma-"

def Burmese.Negation.negSuffix : String

The Burmese negative suffix (replaces TAM markers). Component of the bipartite ma-...-bu circumfix.

Equations

• Burmese.Negation.negSuffix = "-bu"

def Burmese.Negation.circumfix : Syntax.Negation.NegMarkerEntry

ma-...-bu — Burmese's bipartite negation circumfix. The prefix attaches to the verb stem; the suffix replaces the affirmative TAM markers (realis -deh, irrealis -meh, future -laimeh), neutralizing TAM distinctions. WALS classifies Burmese as .doubleNegation (Ch 112A).

Equations

• Burmese.Negation.circumfix = { form := "ma-...-bu", morphemeType := Syntax.Negation.NegMorphemeType.doubleNeg, position := Syntax.Negation.NegMarkerPosition.discontinuous }

def Burmese.Negation.negationSystem : Syntax.Negation.NegationSystem

The Burmese negation system: a single bipartite circumfix. The Fragment-side joint consumed by Studies/Dryer2013Negation.lean.

Equations

• Burmese.Negation.negationSystem = Syntax.Negation.NegationSystem.ofISO "mya" [Burmese.Negation.circumfix]

structure Burmese.Negation.NegParadigmEntry : Type

A Burmese negation paradigm entry showing TAM neutralization.

• tamLabel : String
• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String

def Burmese.Negation.instReprNegParadigmEntry.repr : NegParadigmEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Burmese.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

• Burmese.Negation.instReprNegParadigmEntry = { reprPrec := Burmese.Negation.instReprNegParadigmEntry.repr }

@[implicit_reducible]

instance Burmese.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

• Burmese.Negation.instBEqNegParadigmEntry = { beq := Burmese.Negation.instBEqNegParadigmEntry.beq }

def Burmese.Negation.instBEqNegParadigmEntry.beq : NegParadigmEntry → NegParadigmEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Burmese.Negation.instBEqNegParadigmEntry.beq x✝¹ x✝ = false

def Burmese.Negation.saParadigm : List NegParadigmEntry

Paradigm for sa 'eat'.

Equations

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

structure Burmese.Negation.TAMAvailability : Type

Which TAM categories are available in affirmative vs negative.

• affirmativeTAM : List String

  TAM distinctions available in affirmative

• negativeTAM : List String

  TAM distinctions available in negative

def Burmese.Negation.instReprTAMAvailability.repr : TAMAvailability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Burmese.Negation.instReprTAMAvailability : Repr TAMAvailability

Equations

• Burmese.Negation.instReprTAMAvailability = { reprPrec := Burmese.Negation.instReprTAMAvailability.repr }

@[implicit_reducible]

instance Burmese.Negation.instBEqTAMAvailability : BEq TAMAvailability

Equations

• Burmese.Negation.instBEqTAMAvailability = { beq := Burmese.Negation.instBEqTAMAvailability.beq }

def Burmese.Negation.instBEqTAMAvailability.beq : TAMAvailability → TAMAvailability → Bool

Equations

• Burmese.Negation.instBEqTAMAvailability.beq { affirmativeTAM := a, negativeTAM := a_1 } { affirmativeTAM := b, negativeTAM := b_1 } = (a == b && a_1 == b_1)
• Burmese.Negation.instBEqTAMAvailability.beq x✝¹ x✝ = false

def Burmese.Negation.burmeseTAM : TAMAvailability

Equations

• Burmese.Negation.burmeseTAM = { affirmativeTAM := ["realis", "irrealis", "future"], negativeTAM := ["general negative"] }

Verification

theorem Burmese.Negation.sa_paradigm_size : saParadigm.length = 3

theorem Burmese.Negation.tam_neutralized : have negForms := List.map (fun (x : NegParadigmEntry) => x.negative) saParadigm; (negForms.all fun (x : String) => x == "ma-sa-bu") = true

All negative forms are identical: TAM is neutralized.

theorem Burmese.Negation.paradigmatic_asymmetry : burmeseTAM.affirmativeTAM.length = 3 ∧ burmeseTAM.negativeTAM.length = 1

The affirmative has 3 distinct TAM forms; the negative has 1.

theorem Burmese.Negation.affirmative_forms_distinct : have affForms := List.map (fun (x : NegParadigmEntry) => x.affirmative) saParadigm; affForms.length = 3 ∧ affForms.eraseDups.length = 3

All affirmative forms are distinct (3 TAM contrasts).

def Burmese.Negation.negationProfile : Syntax.Negation.NegationProfile

Burmese negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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