Abstract resource accounting for the v5 hierarchical policy

This module formalizes the manuscript's real-arithmetic accounting model. One primitive arithmetic operation, comparison, or constant-time tree access costs one unit. A period visits one root-to-leaf path. Memory consists of one word for each labeled supply and a constant number of words per tree leaf.

These are mathematical accounting functions, not runtime measurements of Lean's noncomputable definitions.

def FD1D.V5.hierarchicalOperationCount (m : ℕ) : ℕ

Abstract primitive-operation count for one period.

Equations

• FD1D.V5.hierarchicalOperationCount m = 20 * (FD1D.V5.treeDepth m + 1)

def FD1D.V5.hierarchicalMemoryCount (m : ℕ) : ℕ

Abstract memory count for labeled supplies and complete-tree data.

Equations

• FD1D.V5.hierarchicalMemoryCount m = m + 4 * FD1D.V5.leafCount m

theorem FD1D.V5.hierarchicalOperationCount_le_clog {m : ℕ} (hm : 1 ≤ m) : hierarchicalOperationCount m ≤ 20 * (Nat.clog 2 (m + 1) + 1)

Operations are bounded by a constant times the base-two ceiling logarithm.

theorem FD1D.V5.hierarchicalMemoryCount_le_five_mul {m : ℕ} (hm : 1 ≤ m) : hierarchicalMemoryCount m ≤ 5 * m

The abstract memory budget is at most 5m words.

theorem FD1D.V5.hierarchicalOperationCount_cast_le_log {m : ℕ} (hm : 2 ≤ m) : ↑(hierarchicalOperationCount m) ≤ 100 / Real.log 2 * Real.log ↑m

Explicit natural-log bound for the real-valued operation count.

theorem FD1D.V5.hierarchicalOperationCount_isBigO_log : (fun (m : ℕ) => ↑(hierarchicalOperationCount m)) =O[Filter.atTop] fun (m : ℕ) => Real.log ↑m

Per-period operations are O(log m) in the accounting model.

theorem FD1D.V5.hierarchicalMemoryCount_isBigO_linear : (fun (m : ℕ) => ↑(hierarchicalMemoryCount m)) =O[Filter.atTop] fun (m : ℕ) => ↑m

Memory is O(m) in the accounting model.

structure FD1D.V5.HierarchicalResourceGuarantees : Prop

Public bundle of the manuscript's operation and memory guarantees.

• operationsExplicit {m : ℕ} : 2 ≤ m → ↑(hierarchicalOperationCount m) ≤ 100 / Real.log 2 * Real.log ↑m
• memoryExplicit {m : ℕ} : 1 ≤ m → hierarchicalMemoryCount m ≤ 5 * m
• operationsAsymptotic : (fun (m : ℕ) => ↑(hierarchicalOperationCount m)) =O[Filter.atTop] fun (m : ℕ) => Real.log ↑m
• memoryAsymptotic : (fun (m : ℕ) => ↑(hierarchicalMemoryCount m)) =O[Filter.atTop] fun (m : ℕ) => ↑m

theorem FD1D.V5.hierarchicalPolicy_resourceGuarantees : HierarchicalResourceGuarantees