PlacementMoment.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.CoordinateSweeps.Grid.Holes.Placement line 19
def OAI.CoordinateSweeps.Grid.Holes.placementAction line 21
def OAI.CoordinateSweeps.Grid.Holes.placementChart line 24
lemma OAI.CoordinateSweeps.Grid.Holes.placementAction_apply line 33
lemma OAI.CoordinateSweeps.Grid.Holes.placement_valid line 36
lemma OAI.CoordinateSweeps.Grid.Holes.pointFix_iff line 43
def OAI.CoordinateSweeps.Grid.Holes.augmentFixEquiv line 60
Source comment
The point--placement stabilizer is the literal stabilizer of all augmented holes, not an abstract group with the same cardinality.
```
def augmentFixEquiv : (H.placementChart u).pointFix x ≃*
    (H.augment (fun i => (x i).val) v (H.placement_valid x) ω₀ h₀ hv).stabilizer where
…
```
Mentions: OAI.CoordinateSweeps.Grid.Holes.stabilizer
def OAI.CoordinateSweeps.Grid.Holes.augmented line 84
lemma OAI.CoordinateSweeps.Grid.Holes.augmented_compatible line 88
def OAI.CoordinateSweeps.Grid.Holes.augmentedReference line 94
lemma OAI.CoordinateSweeps.Grid.Holes.augmented_feasible line 98
lemma OAI.CoordinateSweeps.Grid.Holes.transition_event line 101
def OAI.CoordinateSweeps.Grid.Holes.augmentedChoices line 121
Source comment
Conditioning on a placement transition is exactly conditioning on the full, unique augmented coordinate paths, not an endpoint approximation.
```
def augmentedChoices (hf : H.Feasible) (x : H.Placement (k := k))
…
```
lemma OAI.CoordinateSweeps.Grid.Holes.augmented_residual line 134
Source comment
A concrete cardinal-free group identity behind the conditional-fiber frame.
```
lemma augmented_residual (hf : H.Feasible) (u x : H.Placement (k := k))
…
```
def OAI.CoordinateSweeps.Grid.Holes.placementWeight line 154
lemma OAI.CoordinateSweeps.Grid.Holes.placementWeight_nonneg line 157
lemma OAI.CoordinateSweeps.Grid.Holes.placementWeight_sum line 161
theorem OAI.CoordinateSweeps.Grid.Holes.transition_probability line 169
Source comment
Transition probability in the induced representation is the exact conditional probability of the augmented path family.
```
theorem transition_probability (hf : H.Feasible) (u x : H.Placement (k := k))
…
```
def OAI.CoordinateSweeps.Grid.Holes.augmentedIrrep line 191
lemma OAI.CoordinateSweeps.Grid.Holes.augmentedIrrep_residual line 197
theorem OAI.CoordinateSweeps.Grid.Holes.transitionAverage_eq_augmented line 216
Source comment
Actual normalized placement-fiber average equals the augmented sweep average in a feasible frame. No conditional law is extended to complex z.
```
theorem transitionAverage_eq_augmented (hf : H.Feasible) (u x : H.Placement (k := k))
…
```
theorem OAI.CoordinateSweeps.Grid.Holes.conditionalBlock_augmented_moment line 242
Source comment
The original conditional fiber moment in06:eq23, with the full augmented path potential available from03:eq4. All frame factors are proved unitary.
```
theorem conditionalBlock_augmented_moment (hf : H.Feasible) (u x : H.Placement (k := k))
…
```
lemma OAI.CoordinateSweeps.Grid.Holes.augmented_extends line 259
theorem OAI.CoordinateSweeps.Grid.Holes.augmented_block_budget line 265
Source comment
The uniform hook estimate is charged to each actual induced block using source03:eq4. This is the precise attachment, not a new assumption about frames.
```
theorem augmented_block_budget (hf : H.Feasible) (u : H.Placement (k := k))
…
```
theorem OAI.CoordinateSweeps.PlacementInduction.Chart.induced_cycle_bound line 318
Source comment
Source06:eq23 for the genuine induced placement representation and its actual normalized blocks. Frobenius reciprocity supplies the literal branching multiplicity.
```
theorem induced_cycle_bound (ρ : UnitaryIrrep C.stabilizer) (τ : UnitaryIrrep G)
    (w : W → ℝ) (hw : ∀ ω, 0 ≤ w ω) (g : W → G) (q : ℕ) (hq : 0 < q) :
    let A := averageMatrix (C.action ρ) (fun ω => (w ω : ℂ)) g
…
```
Mentions: OAI.CoordinateSweeps.UnitaryIrrep
def OAI.CoordinateSweeps.tupleSplit line 344
theorem OAI.CoordinateSweeps.sum_tuple_split line 350
def OAI.CoordinateSweeps.chainWeight line 355
theorem OAI.CoordinateSweeps.chainWeight_succ line 359
theorem OAI.CoordinateSweeps.sum_chainWeight line 366
def OAI.CoordinateSweeps.deletedCycle line 381
Source comment
The edge-deleted product from the source; the missing edge is represented by 1, so the empty/one-node case is unambiguous.
```
def deletedCycle {n : ℕ} (P : Fin (n+1) → Ω → Ω → ℝ)
    (x : Fin (n+1) → Ω) (r : Fin (n+1)) : ℝ :=
…
```
theorem OAI.CoordinateSweeps.deletedCycle_last line 386
def OAI.CoordinateSweeps.tupleReindex line 392
theorem OAI.CoordinateSweeps.deletedCycle_rotate line 399
theorem OAI.CoordinateSweeps.sum_deletedCycle line 420
theorem OAI.CoordinateSweeps.prod_deleted_numbers line 435
Source comment
The product identity retains zeros, so the eventual inequality does not silently omit impossible cyclic placement terms.
```
theorem prod_deleted_numbers {n : ℕ} (p : Fin (n+1) → ℝ) :
    (∏ r, ∏ i, if i = r then (1 : ℝ) else p i) = (∏ i, p i)^n := by
…
```
theorem OAI.CoordinateSweeps.cycle_geometric_identity line 451

theorem OAI.CoordinateSweeps.stochastic_cycle_holder line 467

Source comment

Exact scalar cycle bound used after (23); column stochasticity alone suffices. The paper has both row and column stochasticity from bijections.

theorem stochastic_cycle_holder {n : ℕ} (P : Fin (n+1) → Ω → Ω → ℝ)
    (hP0 : ∀ i x y, 0 ≤ P i x y) (hP : ∀ i y, ∑ x, P i x y = 1) :
    (∑ x : Fin (n+1) → Ω, ∏ i, (P i (x i) (x (i+1)))^((n : ℝ)/(n+1))) ≤
      Fintype.card Ω := by
…

theorem OAI.CoordinateSweeps.stochastic_cycle_holder_length line 498

Source comment

Archived scalar cycle inequality with the positive cycle length explicit.

theorem stochastic_cycle_holder_length {N : ℕ} [NeZero N]
    (P : Fin N → Ω → Ω → ℝ) (hP0 : ∀ i x y, 0 ≤ P i x y)
    (hP : ∀ i y, ∑ x, P i x y=1) :
    (∑ x : Fin N → Ω, ∏ i, (P i (x i) (x (i+1)))^(1-(N : ℝ)⁻¹)) ≤ Fintype.card Ω := by
…

lemma OAI.CoordinateSweeps.weighted_root_le line 508

theorem OAI.CoordinateSweeps.cycle_potential_bound line 528

Source comment

Source06:eq24 scalar endgame, with the full trajectory potential charged once locally as P*T ≤ E. No independence or positivity of edges is assumed.

theorem cycle_potential_bound {N : ℕ} [NeZero N]
    (P T : Fin N → Ω → Ω → ℝ) (hP0 : ∀ i y x, 0 ≤ P i y x)
    (hT0 : ∀ i y x, 0 ≤ T i y x) (hP : ∀ i x, ∑ y, P i y x=1)
    {E : ℝ} (hE : 0 ≤ E) (hPT : ∀ i y x, P i y x*T i y x ≤ E) :
    (∑ x : Fin N → Ω, (∏ i, P i (x i) (x (i+1))) *
      ∏ i, (T i (x i) (x (i+1)))^((N : ℝ)⁻¹)) ≤ (Fintype.card Ω : ℝ)*E := by
…

lemma OAI.CoordinateSweeps.BlockCycles.edgeWeight_columns line 560
lemma OAI.CoordinateSweeps.BlockCycles.edge_moment_nonneg line 567
lemma OAI.CoordinateSweeps.BlockCycles.edge_potential line 573

theorem OAI.CoordinateSweeps.BlockCycles.even_potential_bound line 586

Source comment

The genuine matrix placement-cycle bound closes using the literal doubly stochastic transitions and source03's potential budget.

theorem even_potential_bound (q : ℕ) (hq : 0 < q) (A : Matrix (Ω × n) (Ω × n) ℂ)
    (p : Ω → Ω → ℝ) (hp : ∀ y x, 0 ≤ p y x)
    (hc : ∀ x, ∑ y, p y x=1) (hr : ∀ y, ∑ x, p y x=1)
    (K : Ω → Ω → Matrix n n ℂ)
    (hA : ∀ y x, blocks A y x=(p y x : ℂ) • K y x)
    {E : ℝ} (hE : 0 ≤ E)
    (hPT : ∀ y x, p y x*(Matrix.trace (((K y x).conjTranspose*K y x)^q)).re ≤ E) :
    (Matrix.trace ((A.conjTranspose*A)^q)).re ≤ (Fintype.card Ω : ℝ)*E := by
…

Mentions: OAI.CoordinateSweeps.BlockCycles.blocks

theorem OAI.CoordinateSweeps.PlacementInduction.Chart.induced_potential_bound line 615
lemma OAI.CoordinateSweeps.Grid.Holes.placements_card_le line 635
theorem OAI.CoordinateSweeps.Grid.Holes.actual_induced_endgame line 642
Source comment
Source06:eq24's entire placement-counting and potential endgame, with true branching Hom multiplicity and arbitrary feasible holes. The hook estimate is its sole analytic input and will be discharged by the child induction.
```
theorem actual_induced_endgame (hf : H.Feasible) (u : H.Placement (k := k))
…
```