Markov-model experiment

Logbook.md

@@ -1,5 +1,16 @@
 # Leios logbook
 
+## 2025-10-11
+
+### Parameter-sweep experiment for Markovian model
+
+We completed the first set of experiments using the [Markovian model for Leios efficiency](analysis/markov/).
+
+|   |   |
+|---|---|
+| ![Committee and quorum without adversary](analysis/markov/experiments/Committee%20and%20quorum%20without%20adversary.svg) | ![Ideal conditions with adversary](analysis/markov/experiments/Ideal%20conditions%20with%20adversary.svg) |
+| ![Non-ideal network without adversary](analysis/markov/experiments/Non-ideal%20network%20without%20adversary.svg) | ![Protocol parameters without adversary](analysis/markov/experiments/Protocol%20parameters%20without%20adversary.svg) |
+
 ## 2025-10-10
 
 ### Extended analysis of ledger operations

analysis/markov/.gitignore

@@ -1 +1,4 @@
 /.lake
+.ipynb_checkpoints/
+experiments/*.csv.gz
+experiments/*.png

analysis/markov/Linleios/Evolve.lean

@@ -118,5 +118,7 @@ def ebEfficiency (states : Probabilities) : Float :=
 def efficiency (states : Probabilities) : Float :=
   let rb := rbEfficiency states
   let eb := ebEfficiency states
-  let ρ := 12.5 / 0.9
-  (rb + ρ * eb) / (1 + ρ)
+  let rbSize := 0.9
+  let ebSize := 12.0
+  let ρ := ebSize / rbSize
+  (rb * (1 - eb) + ρ * eb) / (1 + ρ)