Documentation

Linglib.Studies.Arad2005

Arad 2005: root-derived vs word-derived, and the locality of root #

interpretation [Ara05]

The √sgr family (her (5) in Ch. 7): one root, six listed formations across verbal and nominal patterns — sagar 'close', hisgir 'extradite', histager 'cocoon oneself', seger 'closure', sograyim 'parentheses', misgeret 'frame'. Multiple Contextualized Meaning is allosemy of the root across patterns (sgr_mcm); the √qlt nominal table (her (28) in Ch. 3) is the second witness (qlt_mcm).

The lexeme grain and the root grain are related by arrows, not identity: no strict hom merges any two of the lexemes into any target — their contextwise interpretations clash (no_strict_merger) — but the six root-derived lexemes lax-merge into the root's Encyclopedia entry (direct_lax_merger): family, not identity.

The denominal verb misger 'to frame' (her (6)) is derived from the noun misgeret, not from the root: no lax hom carries the full lexicon into the root's entry, because misger is not among the root's own realizations in any pattern (misger_blocked) — her interference argument. Its meaning is instead the compositional image of the noun's (misger_locality), while the root-derived lexemes' meanings are unanalyzable atoms (root_derived_atomic) — her locality constraint (8) in Ch. 7: roots are assigned an interpretation at the first category-assigning head, and the interpretation is carried along thereafter.

Main results #

sgr_mcm, qlt_mcm — Multiple Contextualized Meaning as root allosemy.
no_strict_merger — no two sgr-lexemes strict-merge into any target.
direct_lax_merger — the root-derived lexemes lax-merge into the root.
misger_blocked — the denominal verb blocks a lax merger of the full lexicon: it is not a realization of the root.
misger_locality, root_derived_atomic — word-derived meaning is the compositional image of the base noun's; root-derived meanings are atoms.

The √sgr family #

inductive Arad2005.Pattern :

The patterns of the √sgr family ((5)), plus the denominal verb pattern CiCCeC of (6).

caCaC : Pattern
hiCCiC : Pattern
hitCaCCeC : Pattern
ceCeC : Pattern
coCCayim : Pattern
miCCeCet : Pattern
ciCCeC : Pattern

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqPattern :

DecidableEq Pattern

Equations

Arad2005.instDecidableEqPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypePattern :

Fintype Pattern

Equations

Arad2005.instFintypePattern = { elems := { val := ↑Arad2005.Pattern.enumList, nodup := Arad2005.Pattern.enumList_nodup }, complete := Arad2005.instFintypePattern._proof_1 }

@[implicit_reducible]

instance Arad2005.instReprPattern :

Equations

Arad2005.instReprPattern = { reprPrec := Arad2005.instReprPattern.repr }

def Arad2005.instReprPattern.repr :

Pattern → ℕ → Std.Format

Equations

Arad2005.instReprPattern.repr Arad2005.Pattern.caCaC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.caCaC")).group prec✝
Arad2005.instReprPattern.repr Arad2005.Pattern.hiCCiC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.hiCCiC")).group prec✝
Arad2005.instReprPattern.repr Arad2005.Pattern.hitCaCCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.hitCaCCeC")).group prec✝
Arad2005.instReprPattern.repr Arad2005.Pattern.ceCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.ceCeC")).group prec✝
Arad2005.instReprPattern.repr Arad2005.Pattern.coCCayim prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.coCCayim")).group prec✝
Arad2005.instReprPattern.repr Arad2005.Pattern.miCCeCet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.miCCeCet")).group prec✝
Arad2005.instReprPattern.repr Arad2005.Pattern.ciCCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Pattern.ciCCeC")).group prec✝

Instances For

inductive Arad2005.Meaning :

Meanings: the root-derived listed atoms of (5), plus the compositional layer vOf m — 'to do something with an m' — for word-derived verbs.

close : Meaning
extradite : Meaning
cocoonOneself : Meaning
closure : Meaning
parentheses : Meaning
frame : Meaning
vOf (m : Meaning) : Meaning

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqMeaning :

DecidableEq Meaning

Equations

Arad2005.instDecidableEqMeaning = Arad2005.instDecidableEqMeaning.decEq

def Arad2005.instDecidableEqMeaning.decEq (x✝ x✝¹ : Meaning) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[implicit_reducible]

instance Arad2005.instReprMeaning :

Equations

Arad2005.instReprMeaning = { reprPrec := Arad2005.instReprMeaning.repr }

def Arad2005.instReprMeaning.repr :

Meaning → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Arad2005.instReprMeaning.repr Arad2005.Meaning.close prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Meaning.close")).group prec✝
Arad2005.instReprMeaning.repr Arad2005.Meaning.extradite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Meaning.extradite")).group prec✝
Arad2005.instReprMeaning.repr Arad2005.Meaning.closure prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Meaning.closure")).group prec✝
Arad2005.instReprMeaning.repr Arad2005.Meaning.frame prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Meaning.frame")).group prec✝

Instances For

inductive Arad2005.SgrLex :

The seven lexemes: the six root-derived formations of (5) and the noun-derived misger of (6).

sagar : SgrLex
hisgir : SgrLex
histager : SgrLex
seger : SgrLex
sograyim : SgrLex
misgeret : SgrLex
misger : SgrLex

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqSgrLex :

DecidableEq SgrLex

Equations

Arad2005.instDecidableEqSgrLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypeSgrLex :

Fintype SgrLex

Equations

Arad2005.instFintypeSgrLex = { elems := { val := ↑Arad2005.SgrLex.enumList, nodup := Arad2005.SgrLex.enumList_nodup }, complete := Arad2005.instFintypeSgrLex._proof_1 }

def Arad2005.instReprSgrLex.repr :

SgrLex → ℕ → Std.Format

Equations

Arad2005.instReprSgrLex.repr Arad2005.SgrLex.sagar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.sagar")).group prec✝
Arad2005.instReprSgrLex.repr Arad2005.SgrLex.hisgir prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.hisgir")).group prec✝
Arad2005.instReprSgrLex.repr Arad2005.SgrLex.histager prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.histager")).group prec✝
Arad2005.instReprSgrLex.repr Arad2005.SgrLex.seger prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.seger")).group prec✝
Arad2005.instReprSgrLex.repr Arad2005.SgrLex.sograyim prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.sograyim")).group prec✝
Arad2005.instReprSgrLex.repr Arad2005.SgrLex.misgeret prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.misgeret")).group prec✝
Arad2005.instReprSgrLex.repr Arad2005.SgrLex.misger prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.SgrLex.misger")).group prec✝

Instances For

@[implicit_reducible]

instance Arad2005.instReprSgrLex :

Equations

Arad2005.instReprSgrLex = { reprPrec := Arad2005.instReprSgrLex.repr }

inductive Arad2005.Sqrt :

The single root.

sgr : Sqrt

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqSqrt :

DecidableEq Sqrt

Equations

Arad2005.instDecidableEqSqrt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypeSqrt :

Fintype Sqrt

Equations

Arad2005.instFintypeSqrt = { elems := { val := ↑Arad2005.Sqrt.enumList, nodup := Arad2005.Sqrt.enumList_nodup }, complete := Arad2005.instFintypeSqrt._proof_1 }

@[implicit_reducible]

instance Arad2005.instReprSqrt :

Repr Sqrt

Equations

Arad2005.instReprSqrt = { reprPrec := Arad2005.instReprSqrt.repr }

def Arad2005.instReprSqrt.repr :

Sqrt → ℕ → Std.Format

Equations

Arad2005.instReprSqrt.repr Arad2005.Sqrt.sgr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Sqrt.sgr")).group prec✝

Instances For

def Arad2005.SgrLex.form :

SgrLex → String

Each lexeme's form.

Equations

Arad2005.SgrLex.sagar.form = "sagar"
Arad2005.SgrLex.hisgir.form = "hisgir"
Arad2005.SgrLex.histager.form = "histager"
Arad2005.SgrLex.seger.form = "seger"
Arad2005.SgrLex.sograyim.form = "sograyim"
Arad2005.SgrLex.misgeret.form = "misgeret"
Arad2005.SgrLex.misger.form = "misger"

Instances For

def Arad2005.SgrLex.meaning :

SgrLex → Meaning

Each lexeme's meaning: listed atoms for the root-derived six, the compositional 'to frame' for the noun-derived verb.

Equations

Instances For

def Arad2005.sgrLexemes :

Morphology.Realization.Interpreted SgrLex Pattern String Meaning

The lexeme-grain system: each lexeme licensed in its home pattern only.

Equations

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

Instances For

def Arad2005.sgrRoot :

Morphology.Realization.Interpreted Sqrt Pattern String Meaning

The root-grain system: √sgr's own Encyclopedia entry ((5)) — the six direct cells. The denominal pattern CiCCeC is empty: the root has no root-derived formation there.

Equations

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

Instances For

theorem Arad2005.sgr_mcm :

sgrRoot.IsAllosemous Sqrt.sgr

Multiple Contextualized Meaning is root allosemy: √sgr's interpretation varies across patterns.

Grain arrows #

theorem Arad2005.no_strict_merger {R₂ : Type u_1} {C₂ : Type u_2} {T : Morphology.Realization.Interpreted R₂ C₂ String Meaning} (φ : sgrLexemes.Hom T) {l l' : SgrLex} (h : l ≠ l') :

φ.onRoot l ≠ φ.onRoot l'

No strict hom into any target merges two distinct sgr-lexemes: their contextwise interpretations clash at the home cell (Interpreted.Hom.interp_eq_of_onRoot_eq). At the lexeme grain, all seven are genuinely distinct indices.

inductive Arad2005.Direct :

The root-derived sublexicon of (5).

sagar : Direct
hisgir : Direct
histager : Direct
seger : Direct
sograyim : Direct
misgeret : Direct

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqDirect :

DecidableEq Direct

Equations

Arad2005.instDecidableEqDirect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypeDirect :

Fintype Direct

Equations

Arad2005.instFintypeDirect = { elems := { val := ↑Arad2005.Direct.enumList, nodup := Arad2005.Direct.enumList_nodup }, complete := Arad2005.instFintypeDirect._proof_1 }

@[implicit_reducible]

instance Arad2005.instReprDirect :

Equations

Arad2005.instReprDirect = { reprPrec := Arad2005.instReprDirect.repr }

def Arad2005.instReprDirect.repr :

Direct → ℕ → Std.Format

Equations

Arad2005.instReprDirect.repr Arad2005.Direct.sagar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Direct.sagar")).group prec✝
Arad2005.instReprDirect.repr Arad2005.Direct.hisgir prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Direct.hisgir")).group prec✝
Arad2005.instReprDirect.repr Arad2005.Direct.histager prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Direct.histager")).group prec✝
Arad2005.instReprDirect.repr Arad2005.Direct.seger prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Direct.seger")).group prec✝
Arad2005.instReprDirect.repr Arad2005.Direct.sograyim prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Direct.sograyim")).group prec✝
Arad2005.instReprDirect.repr Arad2005.Direct.misgeret prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.Direct.misgeret")).group prec✝

Instances For

def Arad2005.Direct.toSgr :

Direct → SgrLex

The inclusion into the full lexicon.

Equations

Instances For

def Arad2005.sgrDirect :

Morphology.Realization.Interpreted Direct Pattern String Meaning

The lexeme grain restricted to the root-derived six.

Equations

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

Instances For

theorem Arad2005.direct_lax_merger :

Nonempty (sgrDirect.LaxHom sgrRoot)

The six root-derived lexemes lax-merge into the root's Encyclopedia entry: each one's form and meaning are among the root's, at its own pattern. Family membership without identity — the lexeme→√ coarsening arrow.

theorem Arad2005.misger_blocked (φ : sgrLexemes.LaxHom sgrRoot) :

False

The denominal verb blocks the merger (her interference argument): no lax hom carries the full lexicon into the root's entry, because misger is not among √sgr's realizations in any pattern — it enters the family only through the noun misgeret.

Locality ((8)): assigned at first categorization, carried along #

theorem Arad2005.misger_locality :

sgrLexemes.interp SgrLex.misger Pattern.ciCCeC = Finset.image Meaning.vOf (sgrLexemes.interp SgrLex.misgeret Pattern.miCCeCet)

misger's meaning is the compositional image of misgeret's — 'to X' applied to the noun's fixed interpretation, per the locality constraint: the interpretation assigned at the noun's categorization is carried along into the denominal verb.

theorem Arad2005.root_derived_atomic (l : SgrLex) :

l ≠ SgrLex.misger → ∀ (c : Pattern), ∀ m ∈ sgrLexemes.interp l c, Arad2005.Meaning.isDerived✝ m = false

Root-derived meanings are unanalyzable atoms: none is the compositional image of another formation's meaning — they are listed against the root, fixed at first categorization.

The √qlt witness ((28), (61b)) #

inductive Arad2005.QPattern :

√qlt's nominal patterns ((28)) and its two verbal patterns ((61b)).

ceCeC : QPattern
maCCeC : QPattern
miCCaC : QPattern
taCCiC : QPattern
caCeCet : QPattern
p1 : QPattern
p5 : QPattern

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqQPattern :

DecidableEq QPattern

Equations

Arad2005.instDecidableEqQPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypeQPattern :

Fintype QPattern

Equations

Arad2005.instFintypeQPattern = { elems := { val := ↑Arad2005.QPattern.enumList, nodup := Arad2005.QPattern.enumList_nodup }, complete := Arad2005.instFintypeQPattern._proof_1 }

def Arad2005.instReprQPattern.repr :

QPattern → ℕ → Std.Format

Equations

Arad2005.instReprQPattern.repr Arad2005.QPattern.ceCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.ceCeC")).group prec✝
Arad2005.instReprQPattern.repr Arad2005.QPattern.maCCeC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.maCCeC")).group prec✝
Arad2005.instReprQPattern.repr Arad2005.QPattern.miCCaC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.miCCaC")).group prec✝
Arad2005.instReprQPattern.repr Arad2005.QPattern.taCCiC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.taCCiC")).group prec✝
Arad2005.instReprQPattern.repr Arad2005.QPattern.caCeCet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.caCeCet")).group prec✝
Arad2005.instReprQPattern.repr Arad2005.QPattern.p1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.p1")).group prec✝
Arad2005.instReprQPattern.repr Arad2005.QPattern.p5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QPattern.p5")).group prec✝

Instances For

@[implicit_reducible]

instance Arad2005.instReprQPattern :

Equations

Arad2005.instReprQPattern = { reprPrec := Arad2005.instReprQPattern.repr }

inductive Arad2005.QMeaning :

√qlt's listed meanings: qelet 'input', maqlet 'receiver', miqlat 'shelter, asylum', taqlit '(vinyl) record', qaletet 'cassette', qalat 'absorb', hiqlit 'record'.

input : QMeaning
receiver : QMeaning
shelter : QMeaning
vinylRecord : QMeaning
cassette : QMeaning
absorb : QMeaning
recordV : QMeaning

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqQMeaning :

DecidableEq QMeaning

Equations

Arad2005.instDecidableEqQMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypeQMeaning :

Fintype QMeaning

Equations

Arad2005.instFintypeQMeaning = { elems := { val := ↑Arad2005.QMeaning.enumList, nodup := Arad2005.QMeaning.enumList_nodup }, complete := Arad2005.instFintypeQMeaning._proof_1 }

def Arad2005.instReprQMeaning.repr :

QMeaning → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Arad2005.instReprQMeaning.repr Arad2005.QMeaning.input prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QMeaning.input")).group prec✝
Arad2005.instReprQMeaning.repr Arad2005.QMeaning.receiver prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QMeaning.receiver")).group prec✝
Arad2005.instReprQMeaning.repr Arad2005.QMeaning.shelter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QMeaning.shelter")).group prec✝
Arad2005.instReprQMeaning.repr Arad2005.QMeaning.cassette prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QMeaning.cassette")).group prec✝
Arad2005.instReprQMeaning.repr Arad2005.QMeaning.absorb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QMeaning.absorb")).group prec✝
Arad2005.instReprQMeaning.repr Arad2005.QMeaning.recordV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QMeaning.recordV")).group prec✝

Instances For

@[implicit_reducible]

instance Arad2005.instReprQMeaning :

Equations

Arad2005.instReprQMeaning = { reprPrec := Arad2005.instReprQMeaning.repr }

inductive Arad2005.QSqrt :

The single root.

qlt : QSqrt

Instances For

@[implicit_reducible]

instance Arad2005.instDecidableEqQSqrt :

DecidableEq QSqrt

Equations

Arad2005.instDecidableEqQSqrt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Arad2005.instFintypeQSqrt :

Fintype QSqrt

Equations

Arad2005.instFintypeQSqrt = { elems := { val := ↑Arad2005.QSqrt.enumList, nodup := Arad2005.QSqrt.enumList_nodup }, complete := Arad2005.instFintypeQSqrt._proof_1 }

@[implicit_reducible]

instance Arad2005.instReprQSqrt :

Repr QSqrt

Equations

Arad2005.instReprQSqrt = { reprPrec := Arad2005.instReprQSqrt.repr }

def Arad2005.instReprQSqrt.repr :

QSqrt → ℕ → Std.Format

Equations

Arad2005.instReprQSqrt.repr Arad2005.QSqrt.qlt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Arad2005.QSqrt.qlt")).group prec✝

Instances For

def Arad2005.qltRoot :

Morphology.Realization.Interpreted QSqrt QPattern String QMeaning

√qlt's Encyclopedia entry across its seven attested patterns.

Equations

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

Instances For

theorem Arad2005.qlt_mcm :

qltRoot.IsAllosemous QSqrt.qlt

The √qlt table is a second MCM witness: seven patterns, seven listed meanings — root allosemy at scale.