Feature consistency as Birkhoff renormalization

[MCB25]'s account of the syntax–semantics interface replaces a per-feature checking lifecycle (the retired activate → check → erase state machine with a Boolean convergesAtLF-style verdict) by a single recursive map φ₊ — the renormalized character of a Birkhoff factorization over the Connes–Kreimer Hopf algebra of the syntactic object, which "recursively modifies an initially chosen assignment of semantic values so as to incorporate the consistency checking over all substructures" (§3.1.5).

This file instantiates that map for feature consistency in the Boolean (parsing) semiring of §3.5: the target Consistency = {inconsistent, consistent} with ∨/∧. The syntactic object S (a Nonplanar SOLabel subtree, SOLabel = LIToken ⊕ Unit) embeds into the Hopf algebra via ofTree S.val (no head decoration — the single MCB carrier, FreeCommMagma/toNonplanar retired). A local feature character φ is renormalized by the weight-+1 semiring Birkhoff factorization (RootedTree.ConnesKreimer.SemiringRenorm) into the consistency map φ₊.

The Birkhoff machinery is noncomputable (the coproduct goes through Quotient.out), so φ₊ is a specification of consistency, not an executable checker; concrete verdicts are established by structural proof.

Main definitions

• Consistency: the Boolean consistency semiring (MCB §3.5 Boolean parsing).
• SyntacticObject.toCK: the SO → Connes–Kreimer Hopf algebra bridge ofTree S.val.

References

[MCB25] (§3.1.5, §3.5, Def. 3.1.2, Prop. 3.1.9)

The Boolean consistency semiring

inductive Minimalist.Consistency : Type

The Boolean consistency semiring {inconsistent, consistent}: the two-element idempotent commutative semiring with ∨ ("some decomposition is consistent") as addition and ∧ ("all parts agree") as multiplication. The target of the feature-consistency character ([MCB25] §3.5's Boolean parsing semiring).

• inconsistent : Consistency
• consistent : Consistency

@[implicit_reducible]

instance Minimalist.instDecidableEqConsistency : DecidableEq Consistency

Equations

• Minimalist.instDecidableEqConsistency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instReprConsistency : Repr Consistency

Equations

• Minimalist.instReprConsistency = { reprPrec := Minimalist.instReprConsistency.repr }

def Minimalist.instReprConsistency.repr : Consistency → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instInhabitedConsistency : Inhabited Consistency

Equations

• Minimalist.instInhabitedConsistency = { default := Minimalist.instInhabitedConsistency.default }

@[implicit_reducible]

instance Minimalist.instFintypeConsistency : Fintype Consistency

Equations

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

def Minimalist.Consistency.or : Consistency → Consistency → Consistency

Disjunction (+): consistent iff at least one argument is.

Equations

• Minimalist.Consistency.consistent.or x✝ = Minimalist.Consistency.consistent
• x✝.or Minimalist.Consistency.consistent = Minimalist.Consistency.consistent
• x✝¹.or x✝ = Minimalist.Consistency.inconsistent

def Minimalist.Consistency.and : Consistency → Consistency → Consistency

Conjunction (*): consistent iff both arguments are.

Equations

• Minimalist.Consistency.consistent.and Minimalist.Consistency.consistent = Minimalist.Consistency.consistent
• x✝¹.and x✝ = Minimalist.Consistency.inconsistent

@[implicit_reducible]

instance Minimalist.Consistency.instCommSemiring : CommSemiring Consistency

Equations

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

def Minimalist.Consistency.rbId : RotaBaxterSemiring Consistency

The identity Rota–Baxter operator (weight +1) on Consistency ([MCB25] Lemma 3.2.7, R = id): valid because ∨ is idempotent, so the weight-+1 divergence term is absorbed (a ∧ b = (a∧b) ∨ (a∧b) ∨ (a∧b)). On a Boolean target the threshold/ReLU operator collapses to id, since disagreement already is the additive zero inconsistent.

Equations

• Minimalist.Consistency.rbId = { op := AddMonoidHom.id Minimalist.Consistency, rotaBaxter := Minimalist.Consistency.rbId._proof_1 }

The SO → Hopf algebra bridge

noncomputable def Minimalist.SyntacticObject.toCK (S : SyntacticObject) : RootedTree.ConnesKreimer ℕ (RootedTree.Nonplanar SOLabel)

The syntactic object as an element of the Connes–Kreimer Hopf algebra over ℕ: the singleton forest of its underlying nonplanar tree S.val : Nonplanar SOLabel. The base ring is ℕ (every commutative semiring, including Consistency, is an ℕ-algebra; a Boolean target is not a ℤ-algebra). This is the bridge on which a consistency character acts — no head decoration, since the single MCB carrier already is a Nonplanar SOLabel subtype.

Equations

• S.toCK = RootedTree.ConnesKreimer.ofTree ↑S

The feature-consistency map

noncomputable def Minimalist.featureConsistency (φ : RootedTree.ConnesKreimer ℕ (RootedTree.Nonplanar SOLabel) →ₗ[ℕ] Consistency) (RB : RotaBaxterSemiring Consistency) (S : SyntacticObject) : Consistency

The feature-consistency map φ₊ on a syntactic object: the renormalized value of a feature character φ (with weight-+1 Rota–Baxter operator R) at the SO. This is [MCB25]'s "single recursive map [that] recursively modifies an initially chosen assignment of semantic values so as to incorporate the consistency checking over all substructures" — superseding the retired per-feature checking lifecycle.

Equations

• Minimalist.featureConsistency φ RB S = RootedTree.ConnesKreimer.SemiringRenorm.birkhoffPlusTree φ RB ↑S

theorem Minimalist.featureConsistency_eq_convMul (φ : RootedTree.ConnesKreimer ℕ (RootedTree.Nonplanar SOLabel) →ₗ[ℕ] Consistency) (RB : RotaBaxterSemiring Consistency) (hφ : φ 1 = 1) (S : SyntacticObject) : (LinearMap.mul' ℕ Consistency) ((TensorProduct.map (RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinus φ RB).toLinearMap φ) (RootedTree.ConnesKreimer.comulAlgHomN S.toCK)) = featureConsistency φ RB S

The feature-consistency map factors as the semiring Birkhoff convolution φ₊ = φ₋ ⋆ φ ([MCB25] Def. 3.1.6, Prop. 3.1.9): on the SO's Hopf-algebra image S.toCK, the convolution of the Bogolyubov counterterm φ₋ with the character φ recovers the consistency verdict. Needs φ unital.

The head-following feature character ϕ_{Υ,s,h} (MCB Lemma 3.2.5)

[MCB25]'s interface character (Lemma 3.2.5) follows the head: a probe Υ (testing agreement/disagreement with a semantic hypothesis) is applied to the semantic value of the §1.13 selection head h(T) of a tree, with −∞ (here inconsistent) when T has no well-defined head. We instantiate it for features: the probe Υ : LIToken → Consistency tests the head lexical item's features. The head is the genuine selCheckN (Lemma 1.13.7), so the character is grounded in the real selection-driven head, not a stipulation. (This is MCB's §3.2.1 head-following toy model — deliberately the simplest illustration; §3.2.2 refines it via convexity.)

def Minimalist.headProbeTree (Υ : LIToken → Consistency) (T : RootedTree.Nonplanar SOLabel) : Consistency

The head-probe value on a tree Υ_{s,h} ([MCB25] eq. (3.2.1)): the probe Υ applied to T's §1.13 selection head (selCheckN); inconsistent (−∞) when T has no well-defined head (off the endocentric domain).

Equations

• Minimalist.headProbeTree Υ T = (Minimalist.selCheckN T).elim Minimalist.Consistency.inconsistent fun (p : Minimalist.LIToken × List Minimalist.Cat) => Υ p.1

def Minimalist.headProbeMonoidHom (Υ : LIToken → Consistency) : Multiplicative (RootedTree.Forest (RootedTree.Nonplanar SOLabel)) →* Consistency

Υ_{s,h} extended multiplicatively to forests (the semiring character of Lemma 3.2.5): a workspace is consistent iff each of its trees is. Mirrors birkhoffMinusMonoidHom.

Equations

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

noncomputable def Minimalist.headProbeChar (Υ : LIToken → Consistency) : RootedTree.ConnesKreimer ℕ (RootedTree.Nonplanar SOLabel) →ₐ[ℕ] Consistency

The head-following feature character φ = ϕ_{Υ,s,h} ([MCB25] Lemma 3.2.5) as an algebra hom H →ₐ[ℕ] Consistency: the unrenormalized feature assignment whose Birkhoff renormalization is the consistency map.

Equations

• Minimalist.headProbeChar Υ = RootedTree.ConnesKreimer.lift (Minimalist.headProbeMonoidHom Υ)

@[simp]

theorem Minimalist.headProbeChar_apply_of' (Υ : LIToken → Consistency) (F : RootedTree.Forest (RootedTree.Nonplanar SOLabel)) : (headProbeChar Υ) (RootedTree.ConnesKreimer.of' F) = (Multiset.map (headProbeTree Υ) F).prod

@[simp]

theorem Minimalist.headProbeChar_apply_ofTree (Υ : LIToken → Consistency) (T : RootedTree.Nonplanar SOLabel) : (headProbeChar Υ) (RootedTree.ConnesKreimer.ofTree T) = headProbeTree Υ T

theorem Minimalist.headProbeChar_one (Υ : LIToken → Consistency) : (headProbeChar Υ) 1 = 1

noncomputable def Minimalist.headConsistency (Υ : LIToken → Consistency) (S : SyntacticObject) : Consistency

The feature-consistency verdict on a syntactic object ([MCB25] §3.1.5, Lemma 3.2.5/3.2.7): the Birkhoff renormalization (with R = id) of the head-following feature character ϕ_{Υ,s,h}, evaluated at S. This is the "single recursive map [that] incorporates the consistency checking over all substructures" — the replacement for the retired checking lifecycle. consistent iff the head-probe agreements cohere across all substructures of S.

Equations

• Minimalist.headConsistency Υ S = Minimalist.featureConsistency (Minimalist.headProbeChar Υ).toLinearMap Minimalist.Consistency.rbId S

theorem Minimalist.headConsistency_eq_convMul (Υ : LIToken → Consistency) (S : SyntacticObject) : (LinearMap.mul' ℕ Consistency) ((TensorProduct.map (RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinus (headProbeChar Υ).toLinearMap Consistency.rbId).toLinearMap (headProbeChar Υ).toLinearMap) (RootedTree.ConnesKreimer.comulAlgHomN S.toCK)) = headConsistency Υ S

The head-driven consistency verdict factors as the semiring Birkhoff convolution φ₊ = φ₋ ⋆ φ of the head-following character ([MCB25] Def. 3.1.6, Lemma 3.2.7).