structure Frourio.DihedralInfinity : Type

無限二面体群 D_∞ = ⟨u, r | r² = 1, r u r = u⁻¹⟩。 現時点ではプレースホルダ（後で群表示に基づく形式化へ置換）。

instance Frourio.instReprDihedralInfinity : Repr DihedralInfinity

Equations

• Frourio.instReprDihedralInfinity = { reprPrec := Frourio.reprDihedralInfinity✝ }

instance Frourio.instInhabitedDihedralInfinity : Inhabited DihedralInfinity

Equations

• Frourio.instInhabitedDihedralInfinity = { default := { } }

inductive Frourio.DihedralInfinity.Word : Type

無限二面体群の語（簡易表現）。 id, u^n, u^n⋅r の3形を持つ。後で積と簡約を導入する。

• id : Word
• u (n : ℤ) : Word
• ur (n : ℤ) : Word

instance Frourio.DihedralInfinity.instReprWord : Repr Word

Equations

• Frourio.DihedralInfinity.instReprWord = { reprPrec := Frourio.DihedralInfinity.reprWord✝ }

instance Frourio.DihedralInfinity.instDecidableEqWord : DecidableEq Word

Equations

• Frourio.DihedralInfinity.instDecidableEqWord = Frourio.DihedralInfinity.decEqWord✝

def Frourio.DihedralInfinity.Word.mul : Word → Word → Word

無限二面体群語の乗法（簡易ルール）。 後で正規形・簡約と整合性を証明する。

Equations

• Frourio.DihedralInfinity.Word.id.mul x✝ = x✝
• x✝.mul Frourio.DihedralInfinity.Word.id = x✝
• (Frourio.DihedralInfinity.Word.u n).mul (Frourio.DihedralInfinity.Word.u m) = Frourio.DihedralInfinity.Word.u (n + m)
• (Frourio.DihedralInfinity.Word.u n).mul (Frourio.DihedralInfinity.Word.ur m) = Frourio.DihedralInfinity.Word.ur (n + m)
• (Frourio.DihedralInfinity.Word.ur n).mul (Frourio.DihedralInfinity.Word.u m) = Frourio.DihedralInfinity.Word.ur (n - m)
• (Frourio.DihedralInfinity.Word.ur n).mul (Frourio.DihedralInfinity.Word.ur m) = Frourio.DihedralInfinity.Word.u (n - m)

structure Frourio.CrossedProduct (A : Type u_1) [Ring A] (m : ℕ) : Type u_1

スケール作用による交叉積 A ⋊ ℤ^m（プレースホルダ実装）

• base : A
• scales : Fin m → ℤ

instance Frourio.instReprCrossedProduct {A✝ : Type u_1} {inst✝ : Ring A✝} {m✝ : ℕ} [Repr A✝] : Repr (CrossedProduct A✝ m✝)

Equations

• Frourio.instReprCrossedProduct = { reprPrec := Frourio.reprCrossedProduct✝ }

structure Frourio.ZmAction (A : Type u_1) [Ring A] (m : ℕ) : Type u_1

Z^m による A 上の作用を与えるデータ。 act v は環自己準同型（RingEnd）として振る舞うことを仮定する。 ここでは必要最小限の公理のみを与える。

• act : (Fin m → ℤ) → A → A
• act_zero (a : A) : self.act 0 a = a
• act_add (v w : Fin m → ℤ) (a : A) : self.act (v + w) a = self.act v (self.act w a)
• map_one (v : Fin m → ℤ) : self.act v 1 = 1
• map_mul (v : Fin m → ℤ) (a b : A) : self.act v (a * b) = self.act v a * self.act v b
• map_zero (v : Fin m → ℤ) : self.act v 0 = 0
• map_add (v : Fin m → ℤ) (a b : A) : self.act v (a + b) = self.act v a + self.act v b

def Frourio.CrossedProduct.mul {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y : CrossedProduct A m) : CrossedProduct A m

交叉積の乗法（パラメータ化）。 x * y = ⟨x.base * σ(act x.scales) y.base, x.scales + y.scales⟩。

Equations

• Frourio.CrossedProduct.mul σ x y = { base := x.base * σ.act x.scales y.base, scales := x.scales + y.scales }

instance Frourio.instMulCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) : Mul (CrossedProduct A m)

Equations

• Frourio.instMulCrossedProduct σ = { mul := fun (x y : Frourio.CrossedProduct A m) => Frourio.CrossedProduct.mul σ x y }

instance Frourio.instOneCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} : One (CrossedProduct A m)

Equations

• Frourio.instOneCrossedProduct = { one := { base := 1, scales := 0 } }

instance Frourio.instAddCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} : Add (CrossedProduct A m)

Equations

• Frourio.instAddCrossedProduct = { add := fun (x y : Frourio.CrossedProduct A m) => { base := x.base + y.base, scales := x.scales + y.scales } }

instance Frourio.instZeroCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} : Zero (CrossedProduct A m)

Equations

• Frourio.instZeroCrossedProduct = { zero := { base := 0, scales := 0 } }

instance Frourio.instNegCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} : Neg (CrossedProduct A m)

Equations

• Frourio.instNegCrossedProduct = { neg := fun (x : Frourio.CrossedProduct A m) => { base := -x.base, scales := fun (i : Fin m) => -x.scales i } }

theorem Frourio.add_assoc_crossed {A : Type u_1} [Ring A] {m : ℕ} (x y z : CrossedProduct A m) : x + y + z = x + (y + z)

theorem Frourio.add_comm_crossed {A : Type u_1} [Ring A] {m : ℕ} (x y : CrossedProduct A m) : x + y = y + x

theorem Frourio.add_left_neg_crossed {A : Type u_1} [Ring A] {m : ℕ} (x : CrossedProduct A m) : -x + x = 0

theorem Frourio.scales_eq_zero_if_left_distrib {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y z : CrossedProduct A m) (h : CrossedProduct.mul σ (x + y) z = CrossedProduct.mul σ x z + CrossedProduct.mul σ y z) : z.scales = 0

分配律が成り立つなら z.scales = 0 を強制する（現在の表現では一般には分配しない）。

theorem Frourio.mul_assoc_mul {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x y z : CrossedProduct A m) : CrossedProduct.mul σ (CrossedProduct.mul σ x y) z = CrossedProduct.mul σ x (CrossedProduct.mul σ y z)

乗法の結合律（ZmAction の公理から従う）。

theorem Frourio.one_mul_mul {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : CrossedProduct A m) : CrossedProduct.mul σ One.one x = x

左単位元（1）の性質。

theorem Frourio.mul_one_mul {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) (x : CrossedProduct A m) : CrossedProduct.mul σ x One.one = x

右単位元（1）の性質。

instance Frourio.instMonoidCrossedProduct {A : Type u_1} [Ring A] {m : ℕ} (σ : ZmAction A m) : Monoid (CrossedProduct A m)

交叉積の乗法に関するモノイド構造。

Equations

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

def Frourio.identityZmAction (A : Type u_1) [Ring A] (m : ℕ) : ZmAction A m

恒等作用による Z^m-作用。

Equations

• Frourio.identityZmAction A m = { act := fun (x : Fin m → ℤ) (a : A) => a, act_zero := ⋯, act_add := ⋯, map_one := ⋯, map_mul := ⋯, map_zero := ⋯, map_add := ⋯ }

def Frourio.FrourioOperator.toZmAction {m : ℕ} (_op : FrourioOperator m) (A : Type u_1) [Ring A] : ZmAction A m

Frourio作用素から Z^m-作用を与える（現段階では自明作用）。 将来的に A を関数環等に特化した上でスケール Λ による作用へ差し替える。

Equations

• _op.toZmAction A = Frourio.identityZmAction A m

noncomputable def Frourio.FrourioOperator.scaleFactor {m : ℕ} (op : FrourioOperator m) (v : Fin m → ℤ) : ℝ

v ∈ ℤ^m に対する合成スケール因子。 exp(∑ᵢ vᵢ log Λᵢ) として定義すると加法が積に対応し、作用の結合が証明しやすい。

Equations

• op.scaleFactor v = Real.exp (∑ i : Fin m, ↑(v i) * Real.log (op.Λ i))

noncomputable def Frourio.FrourioOperator.toZmActionOnFunctions {m : ℕ} (op : FrourioOperator m) (B : Type u_1) [Ring B] : ZmAction (ℝ → B) m

関数環 ℝ → B 上の実スケール作用。

Equations

• op.toZmActionOnFunctions B = { act := fun (v : Fin m → ℤ) (f : ℝ → B) (x : ℝ) => f (op.scaleFactor v * x), act_zero := ⋯, act_add := ⋯, map_one := ⋯, map_mul := ⋯, map_zero := ⋯, map_add := ⋯ }

structure Frourio.IsSigmaDerivation {A : Type u_1} [Ring A] (σ : A →+* A) (δ : A → A) : Prop

σ-微分（σ-derivation）の定義。 δ が積に対して δ(ab) = σ(a)δ(b) + δ(a)b を満たすことを表す。

• map_add (a b : A) : δ (a + b) = δ a + δ b
• map_mul (a b : A) : δ (a * b) = σ a * δ b + δ a * b

theorem Frourio.isSigmaDerivation_zero {A : Type u_1} [Ring A] (σ : A →+* A) : IsSigmaDerivation σ fun (x : A) => 0

δ = 0 は自明な σ-導分。

structure Frourio.OreSystem (A : Type u_1) [CommRing A] : Type (max u_1 (u_2 + 1))

Ore拡大の抽象データ。 E は拡大環、Algebra A E を通して A を埋め込み、記号元 Δ : E を持つ。 基本交換関係 Δ⋅a - σ(a)⋅Δ = δ(a)（右辺は A を E へ持ち上げたもの）を仮定。

• E : Type u_2
• ringE : Ring self.E
• algebraAE : Algebra A self.E
• Δ : self.E
• σ : A →+* A
• δ : A → A
• isSigmaDerivation : IsSigmaDerivation self.σ self.δ
• ore_rel (a : A) : self.Δ * (algebraMap A self.E) a - (algebraMap A self.E) (self.σ a) * self.Δ = (algebraMap A self.E) (self.δ a)

def Frourio.oreExchange {A : Type u_1} [CommRing A] {m : ℕ} (_op : FrourioOperator m) (sys : OreSystem A) : Prop

Ore交換式（詳細化）：与えられたOre系で交換関係が成り立つこと。

Equations

• Frourio.oreExchange _op sys = ∀ (a : A), sys.Δ * (algebraMap A sys.E) a - (algebraMap A sys.E) (sys.σ a) * sys.Δ = (algebraMap A sys.E) (sys.δ a)

def Frourio.FrourioOperator.toTrivialOreSystem {m : ℕ} (_op : FrourioOperator m) (A : Type u_1) [CommRing A] : OreSystem A

Frourio作用素から（非自明Δを持つ）退化Ore系を与える。 E = A, Δ = 1, σ = id, δ = 0。

Equations

• _op.toTrivialOreSystem A = { E := A, ringE := inst✝.toRing, algebraAE := Algebra.id A, Δ := 1, σ := RingHom.id A, δ := fun (x : A) => 0, isSigmaDerivation := ⋯, ore_rel := ⋯ }

def Frourio.oreFromSigma {A : Type u_1} [CommRing A] (σ : A →+* A) : OreSystem A

一般の環自己準同型 σ に対して、Δ = 1, δ(a) = a - σ(a) とする非自明なOre系。

Equations

• Frourio.oreFromSigma σ = { E := A, ringE := inst✝.toRing, algebraAE := Algebra.id A, Δ := 1, σ := σ, δ := fun (a : A) => a - σ a, isSigmaDerivation := ⋯, ore_rel := ⋯ }

noncomputable def Frourio.scaleRingHom (B : Type u_1) [CommRing B] (c : ℝ) : (ℝ → B) →+* ℝ → B

実数スケール c による関数環上の環自己準同型。

Equations

• Frourio.scaleRingHom B c = { toFun := fun (f : ℝ → B) (x : ℝ) => f (c * x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def Frourio.FrourioOperator.toOreSystemOnFunctions {m : ℕ} (op : FrourioOperator m) (B : Type u_1) [CommRing B] (i : Fin m) : OreSystem (ℝ → B)

Frourio作用素のスケール Λ i を用いた、関数環上での非自明Ore系。

Equations

• op.toOreSystemOnFunctions B i = Frourio.oreFromSigma (Frourio.scaleRingHom B (op.Λ i))

noncomputable def Frourio.phiOreSystem : OreSystem ℝ

具体例：ℝ 上の自明Ore系。

Equations

• Frourio.phiOreSystem = (Frourio.BasicFrourioOperator Frourio.φ Frourio.phiOreSystem._proof_1).toTrivialOreSystem ℝ

noncomputable def Frourio.OreSystem.matrixJordanId (A : Type u_1) [CommRing A] : OreSystem A

具体例（非自明 Δ, 自明 σ）: 2×2 Jordan ブロックによる Ore 系。 E = M₂(A), Δ = J, σ = id, δ = 0。標準の algebraMap : A → M₂(A)（スカラー埋め込み） の下で、スカラー行列は中心的に振る舞うため、[Δ, a] = 0 が成り立つ。

Equations

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

noncomputable def Frourio.OreSystem.matrixJordan {A : Type u_1} [CommRing A] (σ : A →+* A) : OreSystem A

Equations

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

def Frourio.matrixJordanDiagProp {A : Type u_1} [CommRing A] (σ : A →+* A) : Prop

Diagonal embedding statement for σ on M₂(A) with Jordan block. This is a statement-level version (no heavy proof or instances): it asserts the existence of an algebra structure sending a to diag(a, σ a) and that the Ore commutator with the Jordan block J vanishes (i.e. δ = 0 suffices). The diagonal matrix is expressed via Matrix.diagonal with entries [a, σ a].

Equations

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

structure Frourio.SigmaPBW (A : Type u_1) [CommRing A] (ι : Type u_2) : Type (max (max u_1 u_2) (u_3 + 1))

Multi-generator σ-PBW extension skeleton. ι indexes the generators Δ i, each equipped with its own ring endomorphism σ i and σ-derivation δ i.

• E : Type u_3
• ringE : Ring self.E
• algebraAE : Algebra A self.E
• Δ : ι → self.E
• σ : ι → A →+* A
• δ : ι → A → A
• isSigmaDerivation (i : ι) : IsSigmaDerivation (self.σ i) (self.δ i)
• ore_rel (i : ι) (a : A) : self.Δ i * (algebraMap A self.E) a - (algebraMap A self.E) ((self.σ i) a) * self.Δ i = (algebraMap A self.E) (self.δ i a)

@[reducible, inline]

abbrev Frourio.CriticalPair (ι : Type u_1) : Type u_1

A diamond-critical pair is just an ordered pair of generator indices.

Equations

• Frourio.CriticalPair ι = (ι × ι)

def Frourio.DiamondCriticalPairs (ι : Type u_1) : Type u_1

Placeholder carrier for a list of critical pairs to be checked.

Equations

• Frourio.DiamondCriticalPairs ι = List (Frourio.CriticalPair ι)

theorem Frourio.ore_rewrite_one {A : Type u_1} [CommRing A] (sys : OreSystem A) (a : A) : sys.Δ * (algebraMap A sys.E) a = (algebraMap A sys.E) (sys.σ a) * sys.Δ + (algebraMap A sys.E) (sys.δ a)

Ore 交換式を右辺へ移項した正規化形：Δ a = σ(a) Δ + δ(a)。

def Frourio.monomial {A : Type u_1} [Ring A] {m : ℕ} (v : Fin m → ℤ) : CrossedProduct A m

交叉積における「単項式」：係数1と指数ベクトル v を持つ元。

Equations

• Frourio.monomial v = { base := 1, scales := v }