PinnedHostCopy.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

From anchor rigidity and body localization to the copy-count bound

The independent row and column orders are represented by er and ec. The geometric hypotheses are rigidity of every ordered anchor64 copy and localization of ordered bodies in their actual host roles.

def OAI.Problem348.Construction.Anchor64Pinned line 19
Source documentation
The precise form of anchor rigidity needed for counting: every ordered anchor copy contains one representative of each group of one common mode.
```
def Anchor64Pinned {h n : ℕ} (er ec : Position h ≃ Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
def OAI.Problem348.Construction.OrderedBodyLocalizes line 29
Source documentation
Localization of bodies in the six actual host modes, using the two orders induced by the chosen enumerations.
```
def OrderedBodyLocalizes {h n : ℕ} (er ec : Position h ≃ Fin n) : Prop :=
…
```
Mentions: OAI.Problem348.Construction.Position
theorem OAI.Problem348.Construction.strictMono_anchorIndex52 line 39
Source documentation
The anchor coordinates form an increasing initial segment of the pattern.
```
theorem strictMono_anchorIndex52 : StrictMono BodySignatures52.anchorIndex := by
…
```
Mentions: OAI.Problem348.BodySignatures52.anchorIndex

theorem OAI.Problem348.Construction.pinned_matching_copy_leaf line 45

Source documentation

Once the prefix of a particular matching copy has been pinned, its body roles and the exact four entries supply the leaf witness.

theorem pinned_matching_copy_leaf {h n : ℕ} (er ec : Position h ≃ Fin n)
    (hbody : OrderedBodyLocalizes er ec)
    (r c : Fin 66 → Position h)
    (hr : StrictMono (fun i => er (r i)))
    (hc : StrictMono (fun j => ec (c j)))
    (hmatch : ∀ i j, host (r i) (c j) = fixedH i j)
    (t : Mode h) (zr zc : Fin 64 → Fin (2 ^ h))
    (hrows : ∀ u, r (BodySignatures52.anchorIndex u) = Sum.inl (t, u, zr u))
    (hcols : ∀ v, c (BodySignatures52.anchorIndex v) = Sum.inl (t, v, zc v)) :
    ∃ z, r 64 = countedLeaf z ∧ c 64 = countedLeaf z := by
…

Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.OrderedBodyLocalizes, OAI.Problem348.Construction.host, OAI.Problem348.fixedH, OAI.Problem348.Construction.Mode, OAI.Problem348.BodySignatures52.anchorIndex, OAI.Problem348.Construction.countedLeaf

theorem OAI.Problem348.Construction.host_raw_localization_of_anchor_pinning line 66
Source documentation
Restrict a fixed-H copy to its genuine anchor64 prefix, apply rigidity, and then use body localization. This is the raw localization premise consumed by host_copyCount_le, with no counting or order-transplant assumptions lost.
```
theorem host_raw_localization_of_anchor_pinning {h n : ℕ}
    (er ec : Position h ≃ Fin n)
    (hpin : Anchor64Pinned er ec) (hbody : OrderedBodyLocalizes er ec)
    (r c : Fin 66 → Position h)
    (hr : StrictMono (fun i => er (r i)))
    (hc : StrictMono (fun j => ec (c j)))
    (hmatch : ∀ i j, host (r i) (c j) = fixedH i j) :
    ∃ z, r 64 = countedLeaf z ∧ c 64 = countedLeaf z := by
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Anchor64Pinned, OAI.Problem348.Construction.OrderedBodyLocalizes, OAI.Problem348.Construction.host, OAI.Problem348.fixedH, OAI.Problem348.Construction.countedLeaf
theorem OAI.Problem348.Construction.host_copyCount_le_of_pinning line 82
Source documentation
Anchor rigidity and body localization imply the integer copy bound.
```
theorem host_copyCount_le_of_pinning {h n : ℕ}
    (er ec : Position h ≃ Fin n)
    (hpin : Anchor64Pinned er ec) (hbody : OrderedBodyLocalizes er ec) :
    copyCount fixedH (hostMatrix er ec) ≤ 2 ^ h * n ^ 130 :=
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Anchor64Pinned, OAI.Problem348.Construction.OrderedBodyLocalizes, OAI.Problem348.copyCount, OAI.Problem348.fixedH, OAI.Problem348.Construction.hostMatrix
theorem OAI.Problem348.Construction.host_copyDensity_le_of_pinning line 89
Source documentation
The normalized upper bound for the counterexample sequence.
```
theorem host_copyDensity_le_of_pinning (h : ℕ)
    (er ec : Position h ≃ Fin ((386 * h + 2) * 2 ^ h))
    (hpin : Anchor64Pinned er ec) (hbody : OrderedBodyLocalizes er ec) :
    (copyCount fixedH (hostMatrix er ec) : ℝ) /
        ((((386 * h + 2) * 2 ^ h : ℕ) : ℝ) ^ 132) ≤
      (1 / (((386 * h + 2 : ℕ) : ℝ) ^ 2)) * (1 / ((2 : ℝ) ^ h)) :=
…
```
Mentions: OAI.Problem348.Construction.Position, OAI.Problem348.Construction.Anchor64Pinned, OAI.Problem348.Construction.OrderedBodyLocalizes, OAI.Problem348.copyCount, OAI.Problem348.fixedH, OAI.Problem348.Construction.hostMatrix