Free commutative magma

The free commutative magma on a type α: planar binary trees with leaves in α (i.e., FreeMagma α) modulo the smallest congruence containing the swap relation a * b ~ b * a.

This is the non-associative, commutative analogue of FreeMonoid / FreeCommMonoid. The corresponding typeclass CommMagma (in Mathlib.Algebra.Group.Defs) is satisfied by FreeCommMagma α, giving us the universal property: any function α → β to a CommMagma-equipped type extends uniquely to a magma homomorphism FreeCommMagma α →ₙ* β.

Mathlib precedents

• Multiset α := Quotient (List.isSetoid α) (Mathlib/Data/Multiset/Defs.lean)
• Sym2 α := Quot (Sym2.Rel α) (Mathlib/Data/Sym/Sym2.lean:100)
• FreeAbelianGroup α := Additive (Abelianization (FreeGroup α)) (Mathlib/GroupTheory/FreeAbelianGroup.lean) — closest analogue: take a free non-commutative thing, commutativize via quotient.

The recursor / lift API mirrors Mathlib/Data/Sym/Sym2.lean lines 123–235 verbatim.

Why a quotient and not a Sym2-style inductive

A direct inductive inductive FreeCommMagma | of | mul : Sym2 _ → _ is rejected by Lean's positivity check (Sym2 is a Quot, and Lean does not allow recursive occurrences under an arbitrary Quot). The quotient construction here is the only viable shape.

Linglib usage

Linglib's SyntacticObject is FreeCommMagma (LIToken ⊕ Nat), with Sum.inl a representing real lexical leaves and Sum.inr n representing trace markers (synthesized by Internal Merge). The SyntacticObject.leaf and SyntacticObject.trace shims preserve the constructor-name distinction at use sites.

Out of scope (deferred)

• DecidableEq and Repr via canonicalization (next file in this Phase 0 sequence; requires [LinearOrder α]).
• Functor / Monad instances.
• length (number of leaves).

inductive FreeMagma.CommRel {α : Type u} : FreeMagma α → FreeMagma α → Prop

The smallest commutativity congruence on FreeMagma α: swap, plus push through both arguments of *. The transitive symmetric closure (computed by Quot) is the actual equivalence relation we quotient by.

Three constructors: swap is the substantive content; mul_left and mul_right push the relation through nested multiplications so that, e.g., (a * b) * c ~ (b * a) * c is derivable. Without these congruence rules, Quot CommRel would only quotient top-level swaps, missing nested commutativity.

• swap {α : Type u} (a b : FreeMagma α) : (a * b).CommRel (b * a)
• mul_left {α : Type u} {a b : FreeMagma α} (h : a.CommRel b) (c : FreeMagma α) : (a * c).CommRel (b * c)
• mul_right {α : Type u} (a : FreeMagma α) {b c : FreeMagma α} (h : b.CommRel c) : (a * b).CommRel (a * c)

@[reducible, inline]

abbrev FreeCommMagma (α : Type u) : Type u

Free commutative magma on α: planar binary trees with leaves in α modulo the smallest congruence containing the swap relation.

Single type parameter, matching mathlib's FreeMagma α shape. The non-associative, commutative analogue of FreeMonoid / FreeCommMonoid.

Declared as abbrev (not def) so that Quot-aware lemmas (Quot.eq, Quot.exists_rep, Quot.recOnSubsingleton, …) fire on FreeCommMagma α without needing an unfold. Mirrors Sym2 α := Quot _ (Mathlib/Data/Sym/Sym2.lean:100).

Universal property: any α → β to a CommMagma-equipped β extends uniquely to FreeCommMagma α →ₙ* β (the lift below).

Equations

• FreeCommMagma α = Quot FreeMagma.CommRel

@[reducible, inline]

abbrev FreeCommMagma.mk {α : Type u} (a : FreeMagma α) : FreeCommMagma α

Public alias for Quot.mk _ on FreeCommMagma α. Use this instead of writing (Quot.mk _ a : FreeCommMagma α) at call sites — the type ascription is inferred. Mirrors Sym2.mk (Sym2.lean:103).

Equations

• FreeCommMagma.mk a = Quot.mk FreeMagma.CommRel a

@[reducible, inline]

abbrev FreeCommMagma.of {α : Type u} (a : α) : FreeCommMagma α

Embed a leaf as a FreeCommMagma. Mirrors FreeMagma.of.

Equations

• FreeCommMagma.of a = FreeCommMagma.mk (FreeMagma.of a)

def FreeCommMagma.mul {α : Type u} : FreeCommMagma α → FreeCommMagma α → FreeCommMagma α

Multiplication on FreeCommMagma α lifted from FreeMagma.mul via Quot.lift₂. The swap-respect proofs are exactly the mul_left and mul_right constructors of CommRel (which is why we need the congruence rules in CommRel).

Equations

• FreeCommMagma.mul = Quot.lift₂ (fun (a b : FreeMagma α) => Quot.mk FreeMagma.CommRel (a * b)) ⋯ ⋯

@[implicit_reducible]

instance FreeCommMagma.instMul {α : Type u} : Mul (FreeCommMagma α)

Equations

• FreeCommMagma.instMul = { mul := FreeCommMagma.mul }

@[simp]

theorem FreeCommMagma.of_mul_of {α : Type u} (a b : α) : FreeCommMagma.of a * FreeCommMagma.of b = FreeCommMagma.mk (FreeMagma.of a * FreeMagma.of b)

@[implicit_reducible]

instance FreeCommMagma.instCommMagma {α : Type u} : CommMagma (FreeCommMagma α)

Headline: multiplication is commutative. The reason this type was constructed.

Equations

• FreeCommMagma.instCommMagma = { toMul := FreeCommMagma.instMul, mul_comm := ⋯ }

def FreeCommMagma.lift {α : Type u} {β : Type v} (f : FreeMagma α → β) (h : ∀ (a b : FreeMagma α), a.CommRel b → f a = f b) : FreeCommMagma α → β

Lift a FreeMagma α → β function that respects CommRel to a FreeCommMagma α → β function. Mirrors Quot.lift.

Equations

• FreeCommMagma.lift f h = Quot.lift f h

@[simp]

theorem FreeCommMagma.lift_mk {α : Type u} {β : Type v} (f : FreeMagma α → β) (h : ∀ (a b : FreeMagma α), a.CommRel b → f a = f b) (a : FreeMagma α) : lift f h (FreeCommMagma.mk a) = f a

theorem FreeCommMagma.sound {α : Type u} {a b : FreeMagma α} (h : a.CommRel b) : FreeCommMagma.mk a = FreeCommMagma.mk b

Lemma form of Quot.sound specialized to FreeCommMagma.

theorem FreeCommMagma.swap {α : Type u} (a b : FreeMagma α) : FreeCommMagma.mk (a * b) = FreeCommMagma.mk (b * a)

Specialized swap: mk (a * b) = mk (b * a) as a named lemma. Mirrors mul_comm on the quotient but stated at the FreeMagma level to spare consumers an induction.

theorem FreeCommMagma.exact {α : Type u} {a b : FreeMagma α} (h : FreeCommMagma.mk a = FreeCommMagma.mk b) : Relation.EqvGen FreeMagma.CommRel a b

The eqv-gen-soundness companion to sound: equality on the quotient extracts a EqvGen CommRel proof. Mirrors Sym2.exact-style API.

theorem FreeCommMagma.ind {α : Type u} {motive : FreeCommMagma α → Prop} (h : ∀ (a : FreeMagma α), motive (Quot.mk FreeMagma.CommRel a)) (t : FreeCommMagma α) : motive t

Induction principle for FreeCommMagma α: to prove motive t for all t : FreeCommMagma α, it suffices to prove it for every Quot.mk _ a with a : FreeMagma α. (Quot's ind propagates through the equivalence automatically since motive is a Prop.)

def FreeCommMagma.recOn {α : Type u} {motive : FreeCommMagma α → Sort u_1} (t : FreeCommMagma α) (h : (a : FreeMagma α) → motive (FreeCommMagma.mk a)) (respect : ∀ (a b : FreeMagma α) (r : a.CommRel b), ⋯ ▸ h a = h b) : motive t

recOn-style elimination for Sort-valued motives. Requires the respect hypothesis explicitly (Quot.recOn obligation).

Equations

• FreeCommMagma.recOn t h respect = Quot.recOn t h respect

@[reducible, inline]

abbrev FreeCommMagma.recOnSubsingleton {α : Type u} {motive : FreeCommMagma α → Sort u_1} [∀ (a : FreeMagma α), Subsingleton (motive (FreeCommMagma.mk a))] (t : FreeCommMagma α) (h : (a : FreeMagma α) → motive (FreeCommMagma.mk a)) : motive t

Subsingleton elimination — the typical shape for Decidable, DecidablePred, and other proof-irrelevant Sort-valued motives. Mirrors Sym2.recOnSubsingleton (Sym2.lean:168). Saves consumers from writing Quot.recOnSubsingleton raw and ascribing the type.

Equations

• FreeCommMagma.recOnSubsingleton t h = Quot.recOnSubsingleton t h

def FreeCommMagma.lift₂ {α : Type u} {β : Type v} (f : FreeMagma α → FreeMagma α → β) (hr : ∀ (a b₁ b₂ : FreeMagma α), b₁.CommRel b₂ → f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ b : FreeMagma α), a₁.CommRel a₂ → f a₁ b = f a₂ b) : FreeCommMagma α → FreeCommMagma α → β

lift₂: lift a binary FreeMagma α → FreeMagma α → β function that respects CommRel on each argument. Mirrors Quot.lift₂.

Equations

• FreeCommMagma.lift₂ f hr hs = Quot.lift₂ f hr hs

@[simp]

theorem FreeCommMagma.lift₂_mk {α : Type u} {β : Type v} (f : FreeMagma α → FreeMagma α → β) (hr : ∀ (a b₁ b₂ : FreeMagma α), b₁.CommRel b₂ → f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ b : FreeMagma α), a₁.CommRel a₂ → f a₁ b = f a₂ b) (a b : FreeMagma α) : lift₂ f hr hs (FreeCommMagma.mk a) (FreeCommMagma.mk b) = f a b

theorem FreeCommMagma.inductionOn₂ {α : Type u} {motive : FreeCommMagma α → FreeCommMagma α → Prop} (t s : FreeCommMagma α) (h : ∀ (a b : FreeMagma α), motive (FreeCommMagma.mk a) (FreeCommMagma.mk b)) : motive t s

Two-argument induction: useful for binary operations. The t-then-s argument order mirrors Sym2.inductionOn₂ so callers can pass binary SOs in their natural left-then-right order.

theorem FreeCommMagma.exists_rep {α : Type u} (t : FreeCommMagma α) : ∃ (a : FreeMagma α), FreeCommMagma.mk a = t

Surjectivity of Quot.mk: every FreeCommMagma α element has some FreeMagma α representative. Useful with obtain.

Basic operations

size is the canonical "number of constructors" measure. Lifts via lift since the underlying FreeMagma.size-equivalent respects swap (addition is commutative).

def FreeCommMagma.size {α : Type u} : FreeCommMagma α → ℕ

size t counts the constructors of any planar representative of t : FreeCommMagma α. Well-defined because addition is commutative (the swap-respecting underlying function).

Equations

• FreeCommMagma.size = FreeCommMagma.lift FreeCommMagma.sizeAux✝ ⋯

@[simp]

theorem FreeCommMagma.size_of {α : Type u} (a : α) : (FreeCommMagma.of a).size = 1

@[simp]

theorem FreeCommMagma.size_mul {α : Type u} (a b : FreeCommMagma α) : (a * b).size = 1 + a.size + b.size

Universal property (CommMagma adjunction)

Any function α → β to a CommMagma-equipped β extends uniquely to a magma homomorphism FreeCommMagma α →ₙ* β. The key step is that FreeMagma.lift f already respects CommRel-swap when β is a CommMagma.

Stated in MulHom-shape (→ₙ*) per the mathlib convention for non-unital homomorphisms.

def FreeCommMagma.liftHom {α : Type u} {β : Type v} [CommMagma β] (f : α → β) : FreeCommMagma α →ₙ* β

Universal property: lift f : α → β to a magma homomorphism FreeCommMagma α →ₙ* β. Mirrors FreeMagma.lift (line ~110 of Mathlib/Algebra/Free.lean).

Equations

• FreeCommMagma.liftHom f = { toFun := FreeCommMagma.lift (FreeMagma.liftAux f) ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeCommMagma.liftHom_of {α : Type u} {β : Type v} [CommMagma β] (f : α → β) (a : α) : (liftHom f) (FreeCommMagma.of a) = f a

Functoriality: map

FreeCommMagma is a functor in α. map f is the lift of of ∘ f to a magma homomorphism — the universal property gives uniqueness.

def FreeCommMagma.map {α : Type u} {β : Type v} (f : α → β) : FreeCommMagma α →ₙ* FreeCommMagma β

Functorial map: map f lifts f : α → β to FreeCommMagma α →ₙ* FreeCommMagma β. The codomain FreeCommMagma β is itself a CommMagma (instance above), so this is just liftHom applied to the of-composed function.

Equations

• FreeCommMagma.map f = FreeCommMagma.liftHom (FreeCommMagma.of ∘ f)

@[simp]

theorem FreeCommMagma.map_of {α : Type u} {β : Type v} (f : α → β) (a : α) : (map f) (FreeCommMagma.of a) = FreeCommMagma.of (f a)

@[simp]

theorem FreeCommMagma.map_mul {α : Type u} {β : Type v} (f : α → β) (l r : FreeCommMagma α) : (map f) (l * r) = (map f) l * (map f) r

Canonicalization → DecidableEq

FreeCommMagma α := Quot CommRel doesn't have a generic DecidableEq instance. The standard mathlib idiom (see Multiset.decidableEq) is to canonicalize: pick a unique representative per equivalence class and reduce equality on the quotient to equality of canonical forms.

For [LinearOrder α] we sort the children of each .mul node by lex order on the underlying FreeMagma trees.

Sym2 gets to enumerate representatives because there are only two, but FreeCommMagma's equivalence classes are exponentially large (n! for n internal nodes), so canonicalization is the only viable route.

def FreeMagma.lexCompare {α : Type u} [LinearOrder α] : FreeMagma α → FreeMagma α → Ordering

Lex comparison on FreeMagma α: leaves sort by α-order, leaves sort before mul nodes, mul nodes recursively (left then right).

Equations

• (FreeMagma.of a).lexCompare (FreeMagma.of b) = compare a b
• (FreeMagma.of a).lexCompare (a_1.mul a_2) = Ordering.lt
• (a.mul a_1).lexCompare (FreeMagma.of a_2) = Ordering.gt
• (l₁.mul r₁).lexCompare (l₂.mul r₂) = (l₁.lexCompare l₂).then (r₁.lexCompare r₂)

theorem FreeMagma.lexCompare_self {α : Type u} [LinearOrder α] (a : FreeMagma α) : a.lexCompare a = Ordering.eq

theorem FreeMagma.lexCompare_eq_iff {α : Type u} [LinearOrder α] (a b : FreeMagma α) : a.lexCompare b = Ordering.eq ↔ a = b

theorem FreeMagma.lexCompare_swap {α : Type u} [LinearOrder α] (a b : FreeMagma α) : a.lexCompare b = (b.lexCompare a).swap

def FreeMagma.normalize {α : Type u} [LinearOrder α] : FreeMagma α → FreeMagma α

Canonical form: recursively sort children at each .mul node by lex order. normalize a is the unique representative of the CommRel-equivalence class of a.

Equations

• (FreeMagma.of a).normalize = FreeMagma.of a
• (l.mul r).normalize = match l.normalize.lexCompare r.normalize with | Ordering.gt => r.normalize * l.normalize | x => l.normalize * r.normalize

@[simp]

theorem FreeMagma.normalize_of {α : Type u} [LinearOrder α] (a : α) : (of a).normalize = of a

theorem FreeMagma.normalize_mul {α : Type u} [LinearOrder α] (l r : FreeMagma α) : (l * r).normalize = match l.normalize.lexCompare r.normalize with | Ordering.gt => r.normalize * l.normalize | x => l.normalize * r.normalize

theorem FreeMagma.normalize_swap_mul {α : Type u} [LinearOrder α] (a b : FreeMagma α) : (a * b).normalize = (b * a).normalize

normalize produces a sorted-children form: at each .mul node of normalize a, the left child does NOT lex-compare-greater than the right child.

theorem FreeMagma.normalize_mul_left {α : Type u} [LinearOrder α] (l₁ l₂ r : FreeMagma α) (h : l₁.normalize = l₂.normalize) : (l₁ * r).normalize = (l₂ * r).normalize

theorem FreeMagma.normalize_mul_right {α : Type u} [LinearOrder α] (l r₁ r₂ : FreeMagma α) (h : r₁.normalize = r₂.normalize) : (l * r₁).normalize = (l * r₂).normalize

theorem FreeMagma.commRel_normalize_eq {α : Type u} [LinearOrder α] (a b : FreeMagma α) (h : a.CommRel b) : a.normalize = b.normalize

normalize is constant on CommRel-related elements. The headline of canonicalization.

def FreeCommMagma.normalize {α : Type u} [LinearOrder α] : FreeCommMagma α → FreeMagma α

Lift normalize to FreeCommMagma α: the normal form of any representative is itself a representative, and equal representatives have equal normal forms.

Equations

• FreeCommMagma.normalize = FreeCommMagma.lift FreeMagma.normalize ⋯

@[simp]

theorem FreeCommMagma.normalize_mk {α : Type u} [LinearOrder α] (a : FreeMagma α) : normalize (Quot.mk FreeMagma.CommRel a) = a.normalize

theorem FreeMagma.eqvGen_normalize {α : Type u} [LinearOrder α] (a : FreeMagma α) : Relation.EqvGen CommRel a a.normalize

Every FreeMagma α element is EqvGen CommRel-related to its normal form. Proven by induction on the tree structure: the leaf case is reflexivity; for .mul l r, lift IH(l) and IH(r) through congruence (mul_left + mul_right), then apply swap if the normalizer reordered.

theorem FreeCommMagma.mk_eq_iff_normalize_eq {α : Type u} [LinearOrder α] (a b : FreeMagma α) : Quot.mk FreeMagma.CommRel a = Quot.mk FreeMagma.CommRel b ↔ a.normalize = b.normalize

Bridge lemma: Quot.mk equality on FreeCommMagma α corresponds exactly to normalize-equality on FreeMagma α.

DecidableEq via direct recursion (the mathlib idiom)

Multiset.decidableEq requires only [DecidableEq α] because List.Perm has a clever direct decision procedure (count each element on both sides). For FreeCommMagma, the analogous fact: each .mul node has exactly 2 children, so (l₁*r₁) ~ (l₂*r₂) iff {l₁, r₁} = {l₂, r₂} as a 2-element multiset, which decomposes to (l₁~l₂ ∧ r₁~r₂) ∨ (l₁~r₂ ∧ r₁~l₂). Recursive and decidable from [DecidableEq α] alone — no [LinearOrder α] needed.

Crucially this works because FreeMagma is non-associative — ((a*b)*c) and (a*(b*c)) are NOT CommRel-equivalent. The equivalence preserves tree structure modulo per-node swap.

This is the mathlib-canonical answer: don't canonicalize when a direct DecidableRel on the equivalence works. The LinearOrder-based canonicalization above is still useful when a normal form is wanted (e.g., Repr), but DecidableEq doesn't need it.

def FreeMagma.nodeCount {α : Type u} : FreeMagma α → ℕ

Constructor count, used as a recursion measure for CommEqv.trans. Public so termination proofs in this namespace can reference it.

Equations

• (FreeMagma.of a).nodeCount = 1
• (l.mul r).nodeCount = 1 + l.nodeCount + r.nodeCount

@[simp]

theorem FreeMagma.nodeCount_of {α : Type u} (a : α) : (of a).nodeCount = 1

@[simp]

theorem FreeMagma.nodeCount_mul {α : Type u} (l r : FreeMagma α) : (l * r).nodeCount = 1 + l.nodeCount + r.nodeCount

def FreeMagma.CommEqv {α : Type u} : FreeMagma α → FreeMagma α → Prop

Recursive equivalence relation matching EqvGen CommRel. At each .mul node, try both pairings of children.

Equations

• (FreeMagma.of a).CommEqv (FreeMagma.of b) = (a = b)
• (FreeMagma.of a).CommEqv (a_1.mul a_2) = False
• (a.mul a_1).CommEqv (FreeMagma.of a_2) = False
• (l₁.mul r₁).CommEqv (l₂.mul r₂) = (l₁.CommEqv l₂ ∧ r₁.CommEqv r₂ ∨ l₁.CommEqv r₂ ∧ r₁.CommEqv l₂)

@[implicit_reducible]

instance FreeMagma.instDecidableCommEqv {α : Type u} [DecidableEq α] (a b : FreeMagma α) : Decidable (a.CommEqv b)

Equations

• One or more equations did not get rendered due to their size.
• (FreeMagma.of a).instDecidableCommEqv (FreeMagma.of b) = FreeMagma.instDecidableCommEqv._aux_1 a b
• (FreeMagma.of a).instDecidableCommEqv (a_1.mul a_2) = isFalse ⋯
• (a.mul a_1).instDecidableCommEqv (FreeMagma.of a_2) = isFalse ⋯

theorem FreeMagma.CommEqv.refl {α : Type u} (a : FreeMagma α) : a.CommEqv a

theorem FreeMagma.CommEqv.symm {α : Type u} {a b : FreeMagma α} : a.CommEqv b → b.CommEqv a

theorem FreeMagma.CommEqv.trans {α : Type u} {a b c : FreeMagma α} : a.CommEqv b → b.CommEqv c → a.CommEqv c

theorem FreeMagma.CommEqv.of_commRel {α : Type u} {a b : FreeMagma α} (h : a.CommRel b) : a.CommEqv b

theorem FreeMagma.commEqv_iff_eqvGen {α : Type u} (a b : FreeMagma α) : a.CommEqv b ↔ Relation.EqvGen CommRel a b

The headline correspondence: CommEqv is exactly the equivalence closure of CommRel. Forward: induction on EqvGen using refl, symm, trans, and of_commRel. Reverse: induction on the recursive structure of CommEqv, lifting through congruence rules.

theorem FreeCommMagma.mk_eq_iff_commEqv {α : Type u} (a b : FreeMagma α) : Quot.mk FreeMagma.CommRel a = Quot.mk FreeMagma.CommRel b ↔ a.CommEqv b

Bridge: Quot.mk equality on FreeCommMagma α corresponds exactly to CommEqv-equivalence on FreeMagma α.

@[implicit_reducible]

instance FreeCommMagma.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (FreeCommMagma α)

DecidableEq from [DecidableEq α] alone, mirroring Multiset.decidableEq. The LinearOrder-based normalize exists above for cases that need a canonical form (e.g., Repr), but DecidableEq doesn't go through it.

Equations

• x.instDecidableEq y = Quot.recOnSubsingleton₂ x y fun (a b : FreeMagma α) => decidable_of_iff (a.CommEqv b) ⋯

Repr — placeholder

FreeCommMagma α doesn't have a canonical printable form without canonicalization ([LinearOrder α] + normalize); printing an arbitrary representative is unsafe (Multiset's strategy at Mathlib/Data/Multiset/Sort.lean:106) and propagates unsafe to every consumer that wants deriving Repr.

This placeholder instance returns the string "<FreeCommMagma>" so that downstream deriving Repr on structures containing FreeCommMagma α fields (e.g., linglib's Derivation { initial : SO }) synthesizes safely. The output is uninformative; substantive printing needs a [LinearOrder α]-based normalize-canonicalized variant in a follow-up.

@[implicit_reducible]

instance FreeCommMagma.instRepr {α : Type u} : Repr (FreeCommMagma α)

Equations

• FreeCommMagma.instRepr = { reprPrec := fun (x : FreeCommMagma α) (x_1 : ℕ) => Std.Format.text "<FreeCommMagma>" }

Sections of the quotient projection Quot.mk : FreeMagma → FreeCommMagma

A section of the projection picks a planar representative (a FreeMagma α) for each nonplanar tree (a FreeCommMagma α). This is the natural primitive for the Externalization models of @cite{marcolli-chomsky-berwick-2025} §1.12.1 (book pp. 105-108): the section σ_L assigns to each abstract syntactic object T ∈ 𝔗_{SO_0} a planar embedding σ_L(T) ∈ 𝔗^{pl}_{SO_0}, language-dependently.

Key properties (MCB §1.12.1):

• The section is a map of sets, NOT a morphism of magmas. Per MCB Lemma 1.13.1 (book p. 124), no morphism of magmas exists from FreeCommMagma α to FreeMagma α — a commutative submagma argument rules it out.
• The section is noncanonical: it depends on choices (e.g., language-specific word-order parameters in linguistics).

Mathlib shape: a section is captured exactly by Function.LeftInverse mk σ on the standard quotient projection. We bundle it into a Section structure for ergonomic field access (downstream HeadFunction etc. embed section_ : Section _ as a single field rather than two).

Downstream uses (forward references):

• Linglib/Theories/Syntax/Minimalist/HeadFunction.lean uses Section (LIToken ⊕ Nat) as the substrate for MCB head functions
• The Section.σ_of keystone lemma absorbs ~13 sites of singleton-class case-analysis into a single application
• Per MCB §1.12.3, σ_L can be lifted to a linear map of vector spaces V(𝔗_{SO_0}) → V(𝔗^{pl}_{SO_0}) — this lift is straightforward via Quot.lift once the algebra-side substrate is in place; Section captures the underlying set-level fact

This abstraction generalizes any future MCB-style "section of a quotient projection" need (e.g. Π_L of MCB eq 1.12.4, second projection).

structure FreeCommMagma.Section (α : Type u) : Type u

A section of the quotient projection Quot.mk : FreeMagma α → FreeCommMagma α, per @cite{marcolli-chomsky-berwick-2025} §1.12.1.

The section σ : FreeCommMagma α → FreeMagma α picks a planar representative for each nonplanar tree. The isSection field witnesses Function.LeftInverse mk σ, i.e. ∀ T, FreeCommMagma.mk (σ T) = T.

Per MCB Lemma 1.13.1, σ is not a morphism of magmas (no such morphism exists from FreeCommMagma α to FreeMagma α). It is a map of sets only. Constructing σ is noncanonical: distinct sections correspond to distinct planar embedding choices.

Equivalent to a (noncomputable) bare (σ, isSection) pair, but bundled for ergonomic field access in downstream structures (e.g. HeadFunction).

• σ : FreeCommMagma α → FreeMagma α

  The underlying section function: assigns a planar representative to each nonplanar tree.

• isSection : Function.LeftInverse FreeCommMagma.mk self.σ

  Section equation: mk is a left inverse of σ, i.e. composing yields id.

theorem FreeCommMagma.Section.injective {α : Type u} (s : Section α) : Function.Injective s.σ

A section is injective: distinct quotient elements have distinct planar representatives. Derived via mathlib's Function.LeftInverse.injective.

noncomputable def FreeCommMagma.Section.out {α : Type u} : Section α

The trivial section via Quot.out: noncomputable (classical choice). Useful as a default when no language-specific section is supplied.

Equations

• FreeCommMagma.Section.out = { σ := Quot.out, isSection := ⋯ }

theorem FreeCommMagma.Section.σ_of {α : Type u} (s : Section α) (a : α) : s.σ (FreeCommMagma.of a) = FreeMagma.of a

The keystone helper for singleton-class proofs.

For any a : α, the section's image of FreeCommMagma.of a has the FreeMagma.of a shape: s.σ (of a) = of a.

Why this lemma exists: downstream consumers (e.g. HeadFunction.head_leaf, outerCat_leaf, checkedSel_leaf, toHc_leaf, ...) repeatedly need to prove f (s.σ (of a)) = expected by case-analysis on s.σ (of a)'s FreeMagma shape — leveraging that the equivalence class of of a under CommRel is a singleton (no swap fires on .of _). Without this lemma, every consumer repeats the same 5-line scaffold:

have hSec := s.isSection (of a)
rw [mk_eq_iff_commEqv] at hSec
match hext : s.σ (of a) with
| .of x => exact ...
| .mul _ _ => exact absurd hSec ...

With this lemma, the consumer just rewrites s.σ (of a) to of a and continues structurally.

Proof: composing mk with s.σ recovers the input (isSection); since the equivalence class of of a is a singleton modulo CommRel, s.σ (of a) must itself be of a.