  94
  95/-! ## Certificate -/
  96
  97structure LocalityCert where
  98  uniform : ∀ (L : ZeroParameterLedger), ∀ n,
  99    L.levels n / L.levels (n + 1) = L.levels 0 / L.levels 1
 100  geometric : ∀ (L : ZeroParameterLedger),
 101    ∃ r : ℝ, r > 0 ∧ ∀ k, L.levels (k + 1) = r * L.levels k
 102
 103theorem locality_cert_exists : Nonempty LocalityCert :=
 104  ⟨{ uniform := fun L => uniform_ratio L
 105     geometric := fun L => locality_from_ledger L }⟩
 106
 107end IndisputableMonolith.Foundation.LocalityFromLedger

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.