Finite dyadic addresses

Finite Boolean paths are convenient for adaptive provenance. Indexed cells are convenient for fixed-depth arithmetic, serialization, and integration. This module provides both views and exact decoding into closed dyadic intervals.

def LeanCert.Core.IntervalDyadic.ValueEq (I J : IntervalDyadic) : Prop

Semantic equality of dyadic intervals, independent of endpoint representation.

Equations

• I.ValueEq J = (I.lo.toRat = J.lo.toRat ∧ I.hi.toRat = J.hi.toRat)

theorem LeanCert.Core.IntervalDyadic.ValueEq.refl (I : IntervalDyadic) : I.ValueEq I

theorem LeanCert.Core.IntervalDyadic.ValueEq.symm {I J : IntervalDyadic} (h : I.ValueEq J) : J.ValueEq I

theorem LeanCert.Core.IntervalDyadic.ValueEq.trans {I J K : IntervalDyadic} (hIJ : I.ValueEq J) (hJK : J.ValueEq K) : I.ValueEq K

theorem LeanCert.Core.IntervalDyadic.ValueEq.mem_iff {I J : IntervalDyadic} (h : I.ValueEq J) (x : ℝ) : x ∈ I ↔ x ∈ J

@[reducible, inline]

abbrev LeanCert.Core.DyadicPath : Type

A finite sequence of left (false) and right (true) decisions.

Equations

• LeanCert.Core.DyadicPath = List Bool

def LeanCert.Core.DyadicPath.index : DyadicPath → ℕ

The ordinary binary integer encoded by a path, most-significant bit first.

Equations

• LeanCert.Core.DyadicPath.index [] = 0
• LeanCert.Core.DyadicPath.index (bit :: rest) = (if bit = true then 2 ^ rest.length else 0) + LeanCert.Core.DyadicPath.index rest

theorem LeanCert.Core.DyadicPath.index_lt_pow_length (path : DyadicPath) : path.index < 2 ^ List.length path

A finite binary path always denotes an index at its depth.

@[simp]

theorem LeanCert.Core.DyadicPath.index_append_false (path : DyadicPath) : (path ++ [false]).index = 2 * path.index

@[simp]

theorem LeanCert.Core.DyadicPath.index_append_true (path : DyadicPath) : (path ++ [true]).index = 2 * path.index + 1

def LeanCert.Core.DyadicPath.decodeByBisection (root : IntervalDyadic) : DyadicPath → IntervalDyadic

Decode a path operationally by following exact interval bisections.

Equations

• LeanCert.Core.DyadicPath.decodeByBisection root [] = root
• LeanCert.Core.DyadicPath.decodeByBisection root (bit :: rest) = LeanCert.Core.DyadicPath.decodeByBisection (if bit = true then root.bisect.2 else root.bisect.1) rest

@[simp]

theorem LeanCert.Core.DyadicPath.decodeByBisection_append_false (root : IntervalDyadic) (path : DyadicPath) : decodeByBisection root (path ++ [false]) = (decodeByBisection root path).bisect.1

@[simp]

theorem LeanCert.Core.DyadicPath.decodeByBisection_append_true (root : IntervalDyadic) (path : DyadicPath) : decodeByBisection root (path ++ [true]) = (decodeByBisection root path).bisect.2

structure LeanCert.Core.DyadicCell : Type

A fixed-depth dyadic cell, with its index bounded by the number of cells.

• depth : ℕ
• index : Fin (2 ^ self.depth)

def LeanCert.Core.instReprDyadicCell.repr : DyadicCell → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Core.instReprDyadicCell : Repr DyadicCell

Equations

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

def LeanCert.Core.instDecidableEqDyadicCell.decEq (x✝ x✝¹ : DyadicCell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanCert.Core.instDecidableEqDyadicCell : DecidableEq DyadicCell

Equations

• LeanCert.Core.instDecidableEqDyadicCell = LeanCert.Core.instDecidableEqDyadicCell.decEq

theorem LeanCert.Core.DyadicCell.ext' {a b : DyadicCell} (hdepth : a.depth = b.depth) (hindex : ↑a.index = ↑b.index) : a = b

Cells are equal when their depths and numeric indices agree.

theorem LeanCert.Core.DyadicCell.ext'_iff {a b : DyadicCell} : a = b ↔ a.depth = b.depth ∧ ↑a.index = ↑b.index

def LeanCert.Core.DyadicCell.root : DyadicCell

The root cell at depth zero.

Equations

• LeanCert.Core.DyadicCell.root = { depth := 0, index := ⟨0, LeanCert.Core.DyadicCell.root._proof_1⟩ }

def LeanCert.Core.DyadicCell.childLeft (cell : DyadicCell) : DyadicCell

The left child has index 2k.

Equations

• cell.childLeft = { depth := cell.depth + 1, index := ⟨2 * ↑cell.index, ⋯⟩ }

def LeanCert.Core.DyadicCell.childRight (cell : DyadicCell) : DyadicCell

The right child has index 2k + 1.

Equations

• cell.childRight = { depth := cell.depth + 1, index := ⟨2 * ↑cell.index + 1, ⋯⟩ }

@[simp]

theorem LeanCert.Core.DyadicCell.childLeft_depth (cell : DyadicCell) : cell.childLeft.depth = cell.depth + 1

@[simp]

theorem LeanCert.Core.DyadicCell.childRight_depth (cell : DyadicCell) : cell.childRight.depth = cell.depth + 1

@[simp]

theorem LeanCert.Core.DyadicCell.childLeft_index (cell : DyadicCell) : ↑cell.childLeft.index = 2 * ↑cell.index

@[simp]

theorem LeanCert.Core.DyadicCell.childRight_index (cell : DyadicCell) : ↑cell.childRight.index = 2 * ↑cell.index + 1

def LeanCert.Core.DyadicCell.ofPath (path : DyadicPath) : DyadicCell

Convert a path into the corresponding bounded fixed-depth cell.

Equations

• LeanCert.Core.DyadicCell.ofPath path = { depth := List.length path, index := ⟨path.index, ⋯⟩ }

@[simp]

theorem LeanCert.Core.DyadicCell.ofPath_depth (path : DyadicPath) : (ofPath path).depth = List.length path

@[simp]

theorem LeanCert.Core.DyadicCell.ofPath_index (path : DyadicPath) : ↑(ofPath path).index = path.index

@[simp]

theorem LeanCert.Core.DyadicCell.ofPath_append_false (path : DyadicPath) : ofPath (path ++ [false]) = (ofPath path).childLeft

@[simp]

theorem LeanCert.Core.DyadicCell.ofPath_append_true (path : DyadicPath) : ofPath (path ++ [true]) = (ofPath path).childRight

def LeanCert.Core.DyadicCell.step (root : IntervalDyadic) (cell : DyadicCell) : Dyadic

Exact width of one cell at this depth.

Equations

• LeanCert.Core.DyadicCell.step root cell = root.width.scale2 (-↑cell.depth)

def LeanCert.Core.DyadicCell.decodeDirect (root : IntervalDyadic) (cell : DyadicCell) : IntervalDyadic

Decode an indexed cell directly from its affine endpoint formula.

Equations

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

@[simp]

theorem LeanCert.Core.DyadicCell.step_toRat (root : IntervalDyadic) (cell : DyadicCell) : (step root cell).toRat = root.width.toRat * 2 ^ (-↑cell.depth)

theorem LeanCert.Core.DyadicCell.step_toRat_nonneg (root : IntervalDyadic) (depth : ℕ) : 0 ≤ (root.width.scale2 (-↑depth)).toRat

The exact step at any depth is nonnegative.

structure LeanCert.Core.DyadicCell.PreparedDyadicLevel : Type

Fixed-depth decoding context with the common cell width prepared once.

• root : IntervalDyadic
• depth : ℕ
• step : Dyadic
• step_eq : self.step = self.root.width.scale2 (-↑self.depth)
• step_nonneg : 0 ≤ self.step.toRat

def LeanCert.Core.DyadicCell.PreparedDyadicLevel.prepare (root : IntervalDyadic) (depth : ℕ) : PreparedDyadicLevel

Prepare the shared arithmetic for every cell at one subdivision depth.

Equations

• LeanCert.Core.DyadicCell.PreparedDyadicLevel.prepare root depth = { root := root, depth := depth, step := root.width.scale2 (-↑depth), step_eq := ⋯, step_nonneg := ⋯ }

def LeanCert.Core.DyadicCell.PreparedDyadicLevel.cellCount (level : PreparedDyadicLevel) : ℕ

Number of cells at the prepared level.

Equations

• level.cellCount = 2 ^ level.depth

def LeanCert.Core.DyadicCell.PreparedDyadicLevel.intervalAt (level : PreparedDyadicLevel) (index : Fin level.cellCount) : IntervalDyadic

Random-access decoding using the shared precomputed cell width.

Equations

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

@[simp]

theorem LeanCert.Core.DyadicCell.PreparedDyadicLevel.intervalAt_lo_toRat (level : PreparedDyadicLevel) (index : Fin level.cellCount) : (level.intervalAt index).lo.toRat = level.root.lo.toRat + level.step.toRat * ↑↑index

@[simp]

theorem LeanCert.Core.DyadicCell.PreparedDyadicLevel.intervalAt_hi_toRat (level : PreparedDyadicLevel) (index : Fin level.cellCount) : (level.intervalAt index).hi.toRat = level.root.lo.toRat + level.step.toRat * (↑↑index + 1)

theorem LeanCert.Core.DyadicCell.PreparedDyadicLevel.intervalAt_valueEq_decodeDirect (level : PreparedDyadicLevel) (index : Fin level.cellCount) : (level.intervalAt index).ValueEq (decodeDirect level.root { depth := level.depth, index := index })

Prepared random access agrees with the original direct decoder.

def LeanCert.Core.DyadicCell.PreparedDyadicLevel.materialize (level : PreparedDyadicLevel) : List IntervalDyadic

Materialize a complete fixed-depth level by advancing adjacent endpoints.

Equations

• level.materialize = LeanCert.Core.DyadicCell.PreparedDyadicLevel.materializeFrom✝ level level.cellCount level.root.lo

@[simp]

theorem LeanCert.Core.DyadicCell.PreparedDyadicLevel.materializeFrom_length (level : PreparedDyadicLevel) (count : ℕ) (lo : Dyadic) : (LeanCert.Core.DyadicCell.PreparedDyadicLevel.materializeFrom✝ level count lo).length = count

@[simp]

theorem LeanCert.Core.DyadicCell.PreparedDyadicLevel.materialize_length (level : PreparedDyadicLevel) : level.materialize.length = level.cellCount

@[simp]

theorem LeanCert.Core.DyadicCell.decodeDirect_lo_toRat (root : IntervalDyadic) (cell : DyadicCell) : (decodeDirect root cell).lo.toRat = root.lo.toRat + (step root cell).toRat * ↑↑cell.index

@[simp]

theorem LeanCert.Core.DyadicCell.decodeDirect_hi_toRat (root : IntervalDyadic) (cell : DyadicCell) : (decodeDirect root cell).hi.toRat = root.lo.toRat + (step root cell).toRat * (↑↑cell.index + 1)

theorem LeanCert.Core.DyadicCell.decodeDirect_width_toRat (root : IntervalDyadic) (cell : DyadicCell) : (decodeDirect root cell).width.toRat = (step root cell).toRat

Direct decoding gives every depth-n cell the root width divided by 2^n.

theorem LeanCert.Core.DyadicCell.childLeft_step_toRat (root : IntervalDyadic) (cell : DyadicCell) : (step root cell.childLeft).toRat = (step root cell).toRat / 2

theorem LeanCert.Core.DyadicCell.childRight_step_toRat (root : IntervalDyadic) (cell : DyadicCell) : (step root cell.childRight).toRat = (step root cell).toRat / 2

theorem LeanCert.Core.DyadicCell.decodeDirect_childLeft (root : IntervalDyadic) (cell : DyadicCell) : (decodeDirect root cell.childLeft).ValueEq (decodeDirect root cell).bisect.1

Directly decoding the left child agrees semantically with bisecting the parent.

theorem LeanCert.Core.DyadicCell.decodeDirect_childRight (root : IntervalDyadic) (cell : DyadicCell) : (decodeDirect root cell.childRight).ValueEq (decodeDirect root cell).bisect.2

Directly decoding the right child agrees semantically with bisecting the parent.

theorem LeanCert.Core.DyadicCell.valueEq_bisect_left {I J : IntervalDyadic} (h : I.ValueEq J) : I.bisect.1.ValueEq J.bisect.1

theorem LeanCert.Core.DyadicCell.valueEq_bisect_right {I J : IntervalDyadic} (h : I.ValueEq J) : I.bisect.2.ValueEq J.bisect.2

theorem LeanCert.Core.DyadicCell.decodeDirect_root (root : IntervalDyadic) : (decodeDirect root DyadicCell.root).ValueEq root

theorem LeanCert.Core.DyadicCell.decodeByBisection_valueEq_decodeDirect (root : IntervalDyadic) (path : DyadicPath) : (DyadicPath.decodeByBisection root path).ValueEq (decodeDirect root (ofPath path))

Recursive bisection and direct affine decoding agree at every finite address.

Closed proof semantics and canonical ownership

def LeanCert.Core.DyadicCell.Ownership.closedCell (root : IntervalDyadic) (depth : ℕ) (index : Fin (2 ^ depth)) : IntervalDyadic

The closed proof cell at a fixed level. This is the interval supplied to certified numerical evaluation.

Equations

• LeanCert.Core.DyadicCell.Ownership.closedCell root depth index = (LeanCert.Core.DyadicCell.PreparedDyadicLevel.prepare root depth).intervalAt index

def LeanCert.Core.DyadicCell.Ownership.Owns (root : IntervalDyadic) (depth : ℕ) (index : Fin (2 ^ depth)) (x : ℝ) : Prop

Canonical ownership assigns a point to the greatest-index closed cell that contains it. Thus an interior seam belongs to the cell on its right, matching the half-open convention [lo, hi), while the final cell retains the root's right endpoint.

Equations

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

def LeanCert.Core.DyadicCell.Ownership.ownerSet (root : IntervalDyadic) (depth : ℕ) (index : Fin (2 ^ depth)) : Set ℝ

The set canonically owned by one fixed-depth cell.

Equations

• LeanCert.Core.DyadicCell.Ownership.ownerSet root depth index = {x : ℝ | LeanCert.Core.DyadicCell.Ownership.Owns root depth index x}

def LeanCert.Core.DyadicCell.Ownership.lastIndex (depth : ℕ) : Fin (2 ^ depth)

The final index of a nonempty dyadic level.

Equations

• LeanCert.Core.DyadicCell.Ownership.lastIndex depth = ⟨2 ^ depth - 1, ⋯⟩

theorem LeanCert.Core.DyadicCell.Ownership.ownerSet_subset_closedCell (root : IntervalDyadic) (depth : ℕ) (index : Fin (2 ^ depth)) : ownerSet root depth index ⊆ (closedCell root depth index).toSet

Canonical ownership never enlarges the closed proof cell.

theorem LeanCert.Core.DyadicCell.Ownership.ownerSet_disjoint {root : IntervalDyadic} {depth : ℕ} {i j : Fin (2 ^ depth)} (hne : i ≠ j) : Disjoint (ownerSet root depth i) (ownerSet root depth j)

Distinct cells cannot canonically own the same point.

theorem LeanCert.Core.DyadicCell.Ownership.not_owns_of_mem_higher {root : IntervalDyadic} {depth : ℕ} {i j : Fin (2 ^ depth)} {x : ℝ} (hij : i < j) (hj : x ∈ closedCell root depth j) : ¬Owns root depth i x

A point contained in a higher-index cell cannot be owned by a lower cell. This is the abstract seam-welding rule.

theorem LeanCert.Core.DyadicCell.Ownership.last_owns_of_mem {root : IntervalDyadic} {depth : ℕ} {x : ℝ} (hx : x ∈ closedCell root depth (lastIndex depth)) : Owns root depth (lastIndex depth) x

Any point in the final closed cell is owned by that cell. In particular, the root's right endpoint remains owned rather than being discarded.

theorem LeanCert.Core.DyadicCell.Ownership.exists_mem_closedCell (root : IntervalDyadic) (depth : ℕ) {x : ℝ} (hx : x ∈ root) : ∃ (index : Fin (2 ^ depth)), x ∈ closedCell root depth index

Every point of the root lies in at least one fixed-depth closed proof cell.

theorem LeanCert.Core.DyadicCell.Ownership.exists_unique_owner (root : IntervalDyadic) (depth : ℕ) {x : ℝ} (hx : x ∈ root) : ∃! index : Fin (2 ^ depth), Owns root depth index x

Every root point has a unique canonical owner at each fixed depth.

theorem LeanCert.Core.DyadicCell.Ownership.mem_ownerSet_of_mem_root (root : IntervalDyadic) (depth : ℕ) {x : ℝ} (hx : x ∈ root) : ∃ (index : Fin (2 ^ depth)), x ∈ ownerSet root depth index

Canonical ownership covers the entire root interval.