Parity.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

Parity

Parity-tree roles, forced leaves, coefficient shapes, and exact unsigned/signed motif expansions.

def OAI.TraceReconstruction.roleWeight line 18
Source documentation
Three roles of an active odd child in the manuscript parity expansion: constant, unsigned motif, and signed motif.
```
def roleWeight (χ σ : ℝ) (r : Fin 3) : ℝ :=
…
```
def OAI.TraceReconstruction.signedRoleCount line 21
def OAI.TraceReconstruction.activeRoleCount line 24
theorem OAI.TraceReconstruction.role_product_expansion line 27
theorem OAI.TraceReconstruction.odd_role_difference line 40
theorem OAI.TraceReconstruction.signedRoleCount_le_active line 58
theorem OAI.TraceReconstruction.odd_roles_singleton_or_branch line 68
Source documentation
A surviving odd node either has a unique active signed motif (the local high-order cancellation case), or at least two active children.
```
theorem odd_roles_singleton_or_branch {n : ℕ} (r : Fin n → Fin 3)
    (hodd : Odd (signedRoleCount r)) :
    (∃ i, r i=2 ∧ ∀ j, j≠i → r j=0) ∨ 2 ≤ activeRoleCount r := by
…
```
Mentions: OAI.TraceReconstruction.signedRoleCount, OAI.TraceReconstruction.activeRoleCount
inductive OAI.TraceReconstruction.BranchingTree line 93
Source documentation
Finite occupied trees with at least two continuing odd children at each positive depth. This records exactly the no-singleton branch of the parity argument; the arity and all extra children remain arbitrary.
```
inductive BranchingTree : ℕ → Type
  | leaf : BranchingTree 0
  | node {b : ℕ} (n : ℕ) (children : Fin n → BranchingTree b) (branch : 2 ≤ n) : BranchingTree (b+1)
```
def OAI.TraceReconstruction.BranchingTree.leafCount line 97
def OAI.TraceReconstruction.BranchingTree.levelCount line 101
theorem OAI.TraceReconstruction.BranchingTree.leafCount_lower line 105
inductive OAI.TraceReconstruction.OccupiedParityTree line 121
Source documentation
A term in the parity expansion retains the occupied ordered shape, all roles, and all extra children, rather than assuming it is binary.
```
inductive OccupiedParityTree : ℕ → Type
  | leaf : OccupiedParityTree 0
  | node {b : ℕ} (n : ℕ) (children : Fin n → OccupiedParityTree b)
      (roles : Fin n → Fin 3) : OccupiedParityTree (b+1)
```
def OAI.TraceReconstruction.OccupiedParityTree.isOdd line 126
def OAI.TraceReconstruction.OccupiedParityTree.leafCount line 130
def OAI.TraceReconstruction.OccupiedParityTree.valid line 135
Source documentation
Only odd-role child terms may acquire an active parent multiplier.
```
def OccupiedParityTree.valid : {b : ℕ} → OccupiedParityTree b → Prop
  | _, .leaf => True
  | _, .node _ children roles =>
      (∀ i, roles i ≠ 0 → (children i).isOdd) ∧ ∀ i, (children i).valid
```
Mentions: OAI.TraceReconstruction.OccupiedParityTree, OAI.TraceReconstruction.OccupiedParityTree.isOdd
def OAI.TraceReconstruction.OccupiedParityTree.noSingleton line 140
theorem OAI.TraceReconstruction.OccupiedParityTree.forced_leaves line 149
Source documentation
The exact forced binary number of selected leaves, with all extra occupied vertices present. The hypotheses here are checked properties of a parity term, not a statistical or construction theorem.
```
theorem OccupiedParityTree.forced_leaves {b : ℕ} (t : OccupiedParityTree b)
    (hv : t.valid) (hn : t.noSingleton) (ho : t.isOdd) : 2^b ≤ t.leafCount := by
…
```
Mentions: OAI.TraceReconstruction.OccupiedParityTree
def OAI.TraceReconstruction.IsMotifValue line 186
Source documentation
The literal unsigned/signed motif values at one child index.
```
def IsMotifValue (χ σ : ℝ) : Prop :=
…
```
def OAI.TraceReconstruction.IsTypeSign line 189
theorem OAI.TraceReconstruction.motif_child_sign line 191
theorem OAI.TraceReconstruction.sign_pow_parity line 198
theorem OAI.TraceReconstruction.arbitrary_role_expansion line 208
Source documentation
Product expansion with an arbitrary three-role scalar per child; the only sign variable is the current vertex type.
```
theorem arbitrary_role_expansion {n : ℕ} (w : Fin n → Fin 3 → ℝ) (τ : ℝ) :
    (∏ i, ∑ a : Fin 3, w i a * (if a=2 then τ else 1)) =
      ∑ a : Fin n → Fin 3, (∏ i, w i (a i))*τ^signedRoleCount a := by
…
```
Mentions: OAI.TraceReconstruction.signedRoleCount
def OAI.TraceReconstruction.bottomRoleWeight line 222
Source documentation
At the last internal level every selected leaf has to be active. Role zero has weight zero; unsigned and signed roles are respectively χ/2 and -σ/2 in (χ-στ)/2.
```
def bottomRoleWeight (χ σ : ℝ) (a : Fin 3) : ℝ :=
…
```
def OAI.TraceReconstruction.internalRoleWeight line 225
theorem OAI.TraceReconstruction.bottomRole_sum line 228
theorem OAI.TraceReconstruction.internalRole_sum line 238
inductive OAI.TraceReconstruction.CoefficientShape line 252
Source documentation
An arbitrary occupied ordered subtree, with motif values at its actual child labels. Depth zero here means a bottom sibling group, so it already has one internal level. No binary-shape assumption is made.
```
inductive CoefficientShape : ℕ → Type
  | bottom (n : ℕ) (χ σ : Fin n → ℝ) : CoefficientShape 0
  | node {b : ℕ} (n : ℕ) (χ σ : Fin n → ℝ)
      (children : Fin n → CoefficientShape b) : CoefficientShape (b+1)

namespace CoefficientShape
```
def OAI.TraceReconstruction.CoefficientShape.Admissible line 259
def OAI.TraceReconstruction.CoefficientShape.eval line 263
def OAI.TraceReconstruction.CoefficientShape.Choice line 267
instance OAI.TraceReconstruction.CoefficientShape.choiceFintype line 271
def OAI.TraceReconstruction.CoefficientShape.termTree line 278
def OAI.TraceReconstruction.CoefficientShape.weight line 282
theorem OAI.TraceReconstruction.CoefficientShape.expansion line 292
Source documentation
Full finite coefficient expansion, before any orientation average or fit-event conditioning. This is the literal algebra behind source the correlated-anchor estimate, the parity roles being retained in every term.
```
theorem expansion {b : ℕ} (t : CoefficientShape b) (ha : t.Admissible)
    {τ : ℝ} (ht : IsTypeSign τ) :
    t.eval τ = ∑ a : t.Choice, t.weight a * (if (t.termTree a).isOdd then τ else 1) := by
…
```
Mentions: OAI.TraceReconstruction.CoefficientShape, OAI.TraceReconstruction.IsTypeSign
theorem OAI.TraceReconstruction.CoefficientShape.term_valid line 335
Source documentation
Nonzero terms automatically satisfy the source active-odd rule.
```
theorem term_valid {b : ℕ} (t : CoefficientShape b) (a : t.Choice)
    (h : t.weight a ≠ 0) : (t.termTree a).valid := by
…
```
Mentions: OAI.TraceReconstruction.CoefficientShape
theorem OAI.TraceReconstruction.CoefficientShape.difference_expansion line 353
Source documentation
The difference of hypotheses consists exactly of odd root terms.
```
theorem difference_expansion {b : ℕ} (t : CoefficientShape b) (ha : t.Admissible) :
    t.eval 1-t.eval (-1) = 2*∑ a : t.Choice,
      if (t.termTree a).isOdd then t.weight a else 0 := by
…
```
Mentions: OAI.TraceReconstruction.CoefficientShape
theorem OAI.TraceReconstruction.CoefficientShape.surviving_leaves line 366
Source documentation
A nonzero surviving term without a singleton odd vertex has the full forced binary number of leaves. This follows from the actual expansion, not an assumed parity interface.
```
theorem surviving_leaves {b : ℕ} (t : CoefficientShape b) (a : t.Choice)
    (hw : t.weight a ≠ 0) (ho : (t.termTree a).isOdd)
    (hn : (t.termTree a).noSingleton) : 2^(b+1) ≤ (t.termTree a).leafCount :=
…
```
Mentions: OAI.TraceReconstruction.CoefficientShape

inductive OAI.TraceReconstruction.OccupiedParityTree.Forced line 381

Source documentation

The actual binary selection sits inside an arbitrary occupied parity term, retaining its unselected children rather than assuming binary input.

inductive Forced : {b : ℕ} → OccupiedParityTree b → Type
  | leaf : Forced .leaf
  | node {b n : ℕ} {children : Fin n → OccupiedParityTree b} {roles : Fin n → Fin 3}
      (a c : Fin n) (hne : a≠c) (ha : roles a≠0) (hc : roles c≠0)
      (left : Forced (children a)) (right : Forced (children c)) :
      Forced (.node n children roles)

/-- Every surviving nonsingleton term has an embedded binary subtree.
The selection depends only on the role-marked shape. -/

Mentions: OAI.TraceReconstruction.OccupiedParityTree

theorem OAI.TraceReconstruction.OccupiedParityTree.forced_nonempty line 390
Source documentation
Every surviving nonsingleton term has an embedded binary subtree. The selection depends only on the role-marked shape.
```
theorem forced_nonempty {b : ℕ} (t : OccupiedParityTree b)
    (hv : t.valid) (hn : t.noSingleton) (ho : t.isOdd) : Nonempty t.Forced := by
…
```
Mentions: OAI.TraceReconstruction.OccupiedParityTree

def OAI.TraceReconstruction.OccupiedParityTree.occupied line 410

Source documentation

Occupied shapes have at least one selected leaf below every vertex.

def occupied : {b : ℕ} → OccupiedParityTree b → Prop
  | _, .leaf => True
  | _, .node n children _ => 0<n ∧ ∀ i, (children i).occupied

/-- Number of vertices at a given distance below the root. -/

Mentions: OAI.TraceReconstruction.OccupiedParityTree

def OAI.TraceReconstruction.OccupiedParityTree.levelCount line 415
Source documentation
Number of vertices at a given distance below the root.
```
def levelCount : {b : ℕ} → OccupiedParityTree b → ℕ → ℕ
  | _, _, 0 => 1
  | _, .leaf, _+1 => 0
  | _, .node _ children _, k+1 => ∑ i, (children i).levelCount k
```
Mentions: OAI.TraceReconstruction.OccupiedParityTree
theorem OAI.TraceReconstruction.OccupiedParityTree.leafCount_pos line 420
theorem OAI.TraceReconstruction.OccupiedParityTree.levelCount_le_leaves line 430

theorem OAI.TraceReconstruction.OccupiedParityTree.sum_two_improvements line 440

Source documentation

Two chosen coordinates supply an additive gain in a finite sum.

theorem sum_two_improvements {ι : Type*} [Fintype ι] [DecidableEq ι]
    (x y : ι → ℕ) {a c : ι} (hne : a≠c) (A B : ℕ)
    (hrest : ∀ i, i≠a → i≠c → x i≤y i)
    (ha : x a+A≤y a+B) (hc : x c+A≤y c+B) :
    (∑ i, x i)+2*A ≤ (∑ i, y i)+2*B := by
…

theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.leaf_lower line 458
theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.level_extra line 472
Source documentation
At every positive nonroot level, each unforced occupied vertex costs an extra leaf. This is the exact combinatorial inequality used when additional (nonbinary) labels are summed in the correlated-anchor estimate.
```
theorem Forced.level_extra {b : ℕ} {t : OccupiedParityTree b} (F : t.Forced)
    (ht : t.occupied) (k : ℕ) :
    t.levelCount k+2^b ≤ t.leafCount+2^k := by
…
```
Mentions: OAI.TraceReconstruction.OccupiedParityTree
theorem OAI.TraceReconstruction.OccupiedParityTree.Forced.nonforced_vertices_le_extra_leaves line 490