JAR: Join-Accumulate Refine

4.9. Balance Thresholds🔗

🔗def
Jar.B_S [j : Jar.JarConfig] : Nat
Jar.B_S [j : Jar.JarConfig] : Nat

B_S via JarConfig.

🔗def
Jar.B_I [j : Jar.JarConfig] : Nat
Jar.B_I [j : Jar.JarConfig] : Nat

B_I via JarConfig.

🔗def
Jar.B_L [j : Jar.JarConfig] : Nat
Jar.B_L [j : Jar.JarConfig] : Nat

B_L via JarConfig.

🔗def
Jar.S_MIN : Nat
Jar.S_MIN : Nat

S : Minimum public service index. GP: 𝖲 = 256.