Checked addressed dyadic frontiers

An inductive tree makes coverage structural. A flat list of paths is convenient for untrusted search, serialization, and parallel replay. This module connects the two with a small checker that reconstructs a tree and accepts only its exact canonical leaf list. Acceptance certifies that the decoded paths form a complete binary cover; correspondence between those paths and any external proof or evaluation records must be maintained by the producer of those records.

inductive LeanCert.Core.DyadicSubdivisionTree : Type

A complete binary subdivision tree. A leaf means that the corresponding closed cell is part of the certificate frontier.

• leaf : DyadicSubdivisionTree
• split (left right : DyadicSubdivisionTree) : DyadicSubdivisionTree

def LeanCert.Core.instReprDyadicSubdivisionTree.repr : DyadicSubdivisionTree → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Core.instReprDyadicSubdivisionTree : Repr DyadicSubdivisionTree

Equations

• LeanCert.Core.instReprDyadicSubdivisionTree = { reprPrec := LeanCert.Core.instReprDyadicSubdivisionTree.repr }

@[instance_reducible]

instance LeanCert.Core.instDecidableEqDyadicSubdivisionTree : DecidableEq DyadicSubdivisionTree

Equations

• LeanCert.Core.instDecidableEqDyadicSubdivisionTree = LeanCert.Core.instDecidableEqDyadicSubdivisionTree.decEq

def LeanCert.Core.instDecidableEqDyadicSubdivisionTree.decEq (x✝ x✝¹ : DyadicSubdivisionTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Core.instDecidableEqDyadicSubdivisionTree.decEq LeanCert.Core.DyadicSubdivisionTree.leaf LeanCert.Core.DyadicSubdivisionTree.leaf = isTrue ⋯
• LeanCert.Core.instDecidableEqDyadicSubdivisionTree.decEq LeanCert.Core.DyadicSubdivisionTree.leaf (left.split right) = isFalse ⋯
• LeanCert.Core.instDecidableEqDyadicSubdivisionTree.decEq (left.split right) LeanCert.Core.DyadicSubdivisionTree.leaf = isFalse ⋯

def LeanCert.Core.DyadicSubdivisionTree.paths : DyadicSubdivisionTree → List DyadicPath

Canonical root-relative paths of all leaves, ordered left to right.

Equations

• LeanCert.Core.DyadicSubdivisionTree.leaf.paths = [[]]
• (a.split a_1).paths = List.map (fun (x : List Bool) => false :: x) a.paths ++ List.map (fun (x : List Bool) => true :: x) a_1.paths

@[simp]

theorem LeanCert.Core.DyadicSubdivisionTree.paths_leaf : leaf.paths = [[]]

@[simp]

theorem LeanCert.Core.DyadicSubdivisionTree.paths_split (left right : DyadicSubdivisionTree) : (left.split right).paths = List.map (fun (x : List Bool) => false :: x) left.paths ++ List.map (fun (x : List Bool) => true :: x) right.paths

theorem LeanCert.Core.DyadicSubdivisionTree.exists_mem_decode (tree : DyadicSubdivisionTree) (root : IntervalDyadic) {x : ℝ} (hx : x ∈ root) : ∃ path ∈ tree.paths, x ∈ DyadicPath.decodeByBisection root path

Every point in the root belongs to at least one closed leaf cell.

def LeanCert.Core.DyadicFrontier.maxDepth : List DyadicPath → ℕ

Maximum submitted path length, used only as reconstruction fuel.

Equations

• LeanCert.Core.DyadicFrontier.maxDepth [] = 0
• LeanCert.Core.DyadicFrontier.maxDepth (path :: rest) = max (List.length path) (LeanCert.Core.DyadicFrontier.maxDepth rest)

def LeanCert.Core.DyadicFrontier.check (leaves : List DyadicPath) : Option DyadicSubdivisionTree

Structurally check a flat, canonically ordered list of addressed leaves. On success the returned tree is a proof-friendly reconstruction of precisely those leaves. This does not independently associate the paths with external leaf evidence.

Equations

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

theorem LeanCert.Core.DyadicFrontier.check_eq_some_paths {leaves : List DyadicPath} {tree : DyadicSubdivisionTree} (hcheck : check leaves = some tree) : tree.paths = leaves

Successful checking pins the reconstructed tree to the submitted paths.

theorem LeanCert.Core.DyadicFrontier.exists_mem_decode_of_check {leaves : List DyadicPath} {tree : DyadicSubdivisionTree} (hcheck : check leaves = some tree) (root : IntervalDyadic) {x : ℝ} (hx : x ∈ root) : ∃ path ∈ leaves, x ∈ DyadicPath.decodeByBisection root path

Golden coverage theorem for an accepted flat frontier.