inductive Muse : Type

8! Sharing Protocol: Converging to Eigenvector Unity -

• Calliope : Muse
• Clio : Muse
• Erato : Muse
• Euterpe : Muse
• Melpomene : Muse
• Polyhymnia : Muse
• Terpsichore : Muse
• Thalia : Muse

instance instReprMuse : Repr Muse

Equations

• instReprMuse = { reprPrec := instReprMuse.repr }

def instReprMuse.repr : Muse → Nat → Std.Format

Equations

• instReprMuse.repr Muse.Calliope prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Calliope")).group prec✝
• instReprMuse.repr Muse.Clio prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Clio")).group prec✝
• instReprMuse.repr Muse.Erato prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Erato")).group prec✝
• instReprMuse.repr Muse.Euterpe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Euterpe")).group prec✝
• instReprMuse.repr Muse.Melpomene prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Melpomene")).group prec✝
• instReprMuse.repr Muse.Polyhymnia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Polyhymnia")).group prec✝
• instReprMuse.repr Muse.Terpsichore prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Terpsichore")).group prec✝
• instReprMuse.repr Muse.Thalia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Muse.Thalia")).group prec✝

instance instBEqMuse : BEq Muse

Equations

• instBEqMuse = { beq := instBEqMuse.beq }

def instBEqMuse.beq : Muse → Muse → Bool

Equations

• instBEqMuse.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instDecidableEqMuse : DecidableEq Muse

Equations

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

instance instInhabitedMuse : Inhabited Muse

Equations

• instInhabitedMuse = { default := instInhabitedMuse.default }

def instInhabitedMuse.default : Muse

Equations

• instInhabitedMuse.default = Muse.Calliope

def allMuses : List Muse

Equations

• allMuses = [Muse.Calliope, Muse.Clio, Muse.Erato, Muse.Euterpe, Muse.Melpomene, Muse.Polyhymnia, Muse.Terpsichore, Muse.Thalia]

structure Reflection : Type

• sender : Muse
• receiver : Muse
• iteration : Nat

instance instReprReflection : Repr Reflection

Equations

• instReprReflection = { reprPrec := instReprReflection.repr }

def instReprReflection.repr : Reflection → Nat → Std.Format

Equations

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

structure EigenState : Type

• iteration : Nat
• entropy : Float
• unity : Float

instance instReprEigenState : Repr EigenState

Equations

• instReprEigenState = { reprPrec := instReprEigenState.repr }

def instReprEigenState.repr : EigenState → Nat → Std.Format

Equations

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

def factorial8 : Nat

Equations

• factorial8 = 40320

def computeEntropy (iter : Nat) : Float

Equations

• computeEntropy iter = 1.0 / (1.0 + iter.toFloat)

def computeUnity (iter : Nat) : Float

Equations

• computeUnity iter = 1.0 - 1.0 / (1.0 + iter.toFloat)

def generateReflection (i : Nat) : Reflection

Equations

• generateReflection i = { sender := allMuses[i % 8]!, receiver := allMuses[i / 8 % 8]!, iteration := i }

def isConverged (state : EigenState) : Bool

Equations

• isConverged state = decide (state.unity > 0.999 ∨ state.iteration ≥ factorial8)

def uraniaUnites (reflections : List Reflection) : EigenState

Equations

• uraniaUnites reflections = { iteration := reflections.length, entropy := computeEntropy reflections.length, unity := computeUnity reflections.length }

theorem factorial8Correct : factorial8 = 40320

theorem unityIncreases (n m : Nat) (h : n < m) : computeUnity n < computeUnity m

theorem entropyDecreases (n m : Nat) (h : n < m) : computeEntropy m < computeEntropy n

theorem eventuallyConverges : ∃ (n : Nat), n ≤ factorial8 ∧ computeUnity n > 0.999

def main : IO Unit

Equations

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