HostCopyBound.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Transfer raw-host copy localization to the fixed counting target

The row and column enumerations are independent. This adapter does not assume that either enumeration preserves an ambient order on the sum type: the raw localization hypothesis uses exactly the two induced finite orders.

def OAI.Problem348.Construction.hostMatrix line 18
Source documentation
The canonical host viewed through independent row/column enumerations.
```
def hostMatrix {h n : ℕ} (er ec : Position h ≃ Fin n) : BinaryMatrix n :=
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.BinaryMatrix
def OAI.Problem348.Construction.countedLeaf line 22
Source documentation
A raw leaf is shared by the plus and minus names on both axes.
```
def countedLeaf {h : ℕ} (z : Fin (2 ^ h)) : Position h :=
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.exists_countedLeaf_of_depth_node line 27
Source documentation
The depth/node conclusion of the mode analysis is exactly a leaf-diagonal witness in the raw-position type, including the shared leaf class.
```
theorem exists_countedLeaf_of_depth_node {h : ℕ} (r c : VariablePosition h)
    (hr : depth r = h) (hc : depth c = h) (hnode : node r = node c) :
    ∃ z, (Sum.inr (Sum.inl r) : Position h) = countedLeaf z ∧
      (Sum.inr (Sum.inl c) : Position h) = countedLeaf z := by
…
```
Mentions: OAI.Problem348.Construction.VariablePosition, OAI.Problem348.Construction.depth, OAI.Problem348.Construction.node, OAI.Problem348.Construction.Position, OAI.Problem348.Construction.countedLeaf

theorem OAI.Problem348.Construction.localization_on_fin line 54

Source documentation

Exact localization of a raw copy transports without any count-equivalence machinery. The increasing-map hypotheses refer to the supplied enumerations.

theorem localization_on_fin {h n : ℕ} (er ec : Position h ≃ Fin n)
    (hloc : ∀ r c : Fin 66 → Position h,
      StrictMono (fun i => er (r i)) → StrictMono (fun j => ec (c j)) →
      (∀ i j, host (r i) (c j) = fixedH i j) →
      ∃ z, r 64 = countedLeaf z ∧ c 64 = countedLeaf z)
    (r c : IncreasingMap 66 n)
    (hentries : ∀ i j, hostMatrix er ec (r.val i) (c.val j) = fixedH i j) :
    ∃ z, r.val 64 = er (countedLeaf z) ∧ c.val 64 = ec (countedLeaf z) := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.host, OAI.Problem348.fixedH, OAI.Problem348.Construction.countedLeaf, OAI.Problem348.IncreasingMap, OAI.Problem348.Construction.hostMatrix

theorem OAI.Problem348.Construction.host_copyCount_le line 70

Source documentation

Integer bound used by the sequence assembly, from raw-host localization.

theorem host_copyCount_le {h n : ℕ} (er ec : Position h ≃ Fin n)
    (hloc : ∀ r c : Fin 66 → Position h,
      StrictMono (fun i => er (r i)) → StrictMono (fun j => ec (c j)) →
      (∀ i j, host (r i) (c j) = fixedH i j) →
      ∃ z, r 64 = countedLeaf z ∧ c 64 = countedLeaf z) :
    copyCount fixedH (hostMatrix er ec) ≤ 2 ^ h * n ^ 130 := by
…

theorem OAI.Problem348.Construction.host_copyDensity_le line 88

Source documentation

The exact density upper bound of counterexample_sequence for this raw host.

theorem host_copyDensity_le (h : ℕ)
    (er ec : Position h ≃ Fin ((386 * h + 2) * 2 ^ h))
    (hloc : ∀ r c : Fin 66 → Position h,
      StrictMono (fun i => er (r i)) → StrictMono (fun j => ec (c j)) →
      (∀ i j, host (r i) (c j) = fixedH i j) →
      ∃ z, r 64 = countedLeaf z ∧ c 64 = countedLeaf z) :
    (copyCount fixedH (hostMatrix er ec) : ℝ) /
        ((((386 * h + 2) * 2 ^ h : ℕ) : ℝ) ^ 132) ≤
      (1 / (((386 * h + 2 : ℕ) : ℝ) ^ 2)) * (1 / ((2 : ℝ) ^ h)) := by
…