Paradigm complexity: entropy and implicative structure over cells

Two views of the Paradigm Cell Filling Problem over a ParadigmSystem. The quantitative layer measures cell distributions: Shannon entropy of a cell, conditional entropy between cells (the integrand of [AM13a]'s i-complexity), and the derived implicative-structure predicates. The qualitative layer is the zero-entropy (categorical) case: a set of cells Predicts another when the forms filling it determine the form filling the target across every inflection class — the implicative relation [BB16] quantify with conditional entropy, here as a plain relation over the system's rows. Entropy quantification stays prose-level per repo discipline; Predicts is its zero-entropy extreme.

Main declarations

• ParadigmSystem.cellEntropy, ParadigmSystem.conditionalCellEntropy
• ParadigmSystem.isImplicative, ParadigmSystem.isTransparent
• ParadigmSystem.Predicts, ParadigmSystem.IsPrincipalPartSet — the categorical implicative relation and principal-part sets

iComplexity (the paper-specific average conditional entropy) and LCECHolds (the LCEC threshold predicate) live in Studies/AckermanMalouf2013.lean because they are particular aggregations the paper defines, not substrate primitives.

noncomputable def Morphology.ParadigmSystem.cellEntropy {n : ℕ} {Form : Type u_1} [DecidableEq Form] (ps : ParadigmSystem n Form) (c : Fin n) : ℝ

Shannon entropy of the empirical distribution at cell c (in nats).

Equations

• ps.cellEntropy c = match Morphology.distOfList✝ (ps.cellDistribution c) with | (support, prob) => Morphology.entropy✝ support prob

noncomputable def Morphology.ParadigmSystem.conditionalCellEntropy {n : ℕ} {Form : Type u_1} [DecidableEq Form] (ps : ParadigmSystem n Form) (ci cj : Fin n) : ℝ

Conditional entropy H(C_i | C_j) of cell ci given cell cj (in nats). The integrand of [AM13a]'s i-complexity.

Equations

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

def Morphology.ParadigmSystem.isImplicative {n : ℕ} {Form : Type u_1} [DecidableEq Form] (ps : ParadigmSystem n Form) (ci cj : Fin n) : Prop

A cell pair (ci, cj) is implicative iff knowing the form at cj perfectly determines the form at ci (zero conditional entropy).

Equations

• ps.isImplicative ci cj = (ps.conditionalCellEntropy ci cj = 0)

def Morphology.ParadigmSystem.isTransparent {n : ℕ} {Form : Type u_1} [DecidableEq Form] (ps : ParadigmSystem n Form) : Prop

A paradigm is transparent iff every off-diagonal cell pair is implicative — every cell perfectly predicts every other.

Equations

• ps.isTransparent = ∀ (ci cj : Fin n), ci ≠ cj → ps.isImplicative ci cj

Qualitative implicative structure

The categorical (zero-entropy) face of the Paradigm Cell Filling Problem [BB16]: which sets of known cells determine an unknown cell across the inflection classes.

def Morphology.ParadigmSystem.Predicts {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) (S : Finset (Fin n)) (j : Fin n) : Prop

A set of cells S predicts cell j when the forms filling S determine the form filling j across the system: any two inflection classes agreeing on every cell of S also agree at j. The zero-conditional-entropy case of the implicative relation [BB16] measure.

Equations

• ps.Predicts S j = ∀ p ∈ ps.entries, ∀ q ∈ ps.entries, (∀ c ∈ S, p.1 c = q.1 c) → p.1 j = q.1 j

def Morphology.ParadigmSystem.IsPrincipalPartSet {n : ℕ} {Form : Type u_1} (ps : ParadigmSystem n Form) (S : Finset (Fin n)) : Prop

A set of cells is a principal-part set when it predicts every cell of the system: knowing those forms determines the whole paradigm.

Equations

• ps.IsPrincipalPartSet S = ∀ (j : Fin n), ps.Predicts S j

theorem Morphology.ParadigmSystem.Predicts.mono {n : ℕ} {Form : Type u_1} {ps : ParadigmSystem n Form} {S T : Finset (Fin n)} {j : Fin n} (hST : S ⊆ T) (h : ps.Predicts S j) : ps.Predicts T j

Prediction is monotone in the known cells: enlarging the predictor set never destroys a prediction.