OAI/Probability/CoordinateSweeps/Attachment.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Work on the genuinely missing main statements of the pinned manuscript. All definitions are finite and use the source's ordinary probability and trace normalizations. No result of the manuscript is assumed.

  1. def OAI.CoordinateSweeps.Grid.Holes.removedPlacement line 30
  2. def OAI.CoordinateSweeps.Grid.Holes.retainedMap line 37
  3. lemma OAI.CoordinateSweeps.Grid.Holes.retainedMap_fixed line 40
  4. def OAI.CoordinateSweeps.Grid.Holes.retainedInto line 50
  5. lemma OAI.CoordinateSweeps.Grid.Holes.retainedInto_bijective line 55
  6. def OAI.CoordinateSweeps.Grid.Holes.retainedEquiv line 89

    Source comment

    Actual retained-hook subgroup chart inside the original hole stabilizer.
    def retainedEquiv : Equiv.Perm (Boxes (hookPart μ p)) ≃*
    (H.placementChart (H.removedPlacement μ p e)).stabilizer :=
…

    Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.Grid.Holes.stabilizer

  7. lemma OAI.CoordinateSweeps.UnitaryIrrep.asRepresentation_pullback line 96
  8. lemma OAI.CoordinateSweeps.UnitaryIrrep.dimension_eq_finrank line 98
  9. def OAI.CoordinateSweeps.Grid.Holes.boxesChart line 106
  10. lemma OAI.CoordinateSweeps.Grid.Holes.retained_restrict line 109
  11. theorem OAI.CoordinateSweeps.Grid.Holes.exists_retained_irrep line 116

    Source comment

    Source06:eq22 and genuine retained-hook Hom multiplicity simultaneously, on the literal placement stabilizer used by the conditional induced cycle.
    theorem exists_retained_irrep (τ : UnitaryIrrep H.stabilizer)
    (hτ : hasShape μ (Equiv.refl _) (τ.pullback (H.boxesChart μ e)).asRepresentation) :
    ∃ ρ : UnitaryIrrep (H.placementChart (H.removedPlacement μ p e)).stabilizer,
      hasShape (hookPart μ p) (Equiv.refl _)
        (ρ.asRepresentation.comp (H.retainedEquiv μ p e).toMonoidHom) ∧
      Module.finrank ℂ (shapeSubrep (removedPart μ p) (Equiv.refl _)).toSubmodule ≤
        Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap
          (matrixRepresentation (τ.matrix.comp (H.placementChart (H.removedPlacement μ p e)).stabilizer.subtype))) ∧
      τ.dimension ≤ (Fintype.card (Boxes μ))^(Fintype.card (Boxes (removedPart μ p)))*ρ.dimension := by
…

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.Grid.Holes.stabilizer

  12. def OAI.CoordinateSweeps.Grid.Holes.retainedSite line 168
  13. lemma OAI.CoordinateSweeps.Grid.Holes.retainedSite_ne_removed line 171
  14. lemma OAI.CoordinateSweeps.Grid.Holes.retainedMap_site line 177
  15. def OAI.CoordinateSweeps.Grid.Holes.augmentedRetainedEmbedding line 185
  16. lemma OAI.CoordinateSweeps.Grid.Holes.augmentedRetainedEmbedding_surjective line 212
  17. def OAI.CoordinateSweeps.Grid.Holes.augmentedRetainedEquiv line 227
  18. def OAI.CoordinateSweeps.Grid.Holes.augmentedRetainedChart line 240
  19. lemma OAI.CoordinateSweeps.Grid.Holes.augmentedRetainedChart_eq line 245
  20. theorem OAI.CoordinateSweeps.Grid.Holes.augmented_hasShape line 274

    Source comment

    The transported fiber is the same retained Young type on the *actual* remaining sites. This rules out any unsupported abstract symmetric-group relabeling.
    theorem augmented_hasShape
    (ρ : UnitaryIrrep (H.placementChart (H.removedPlacement μ p e)).stabilizer)
    (hρ : hasShape (hookPart μ p) (Equiv.refl _)
      (ρ.asRepresentation.comp (H.retainedEquiv μ p e).toMonoidHom))
    (x : H.Placement (k := Fintype.card (Boxes (removedPart μ p))))
…

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.Grid.Holes.stabilizer

  21. theorem OAI.CoordinateSweeps.Grid.Holes.extraProbability_nonneg line 333
  22. theorem OAI.CoordinateSweeps.Grid.Holes.scaled_extraProbability_le line 345

    Source comment

    Faithful finite-event application of the transition comparison: the selected extra paths are appended to the holes only when their joint event is possible.
    theorem scaled_extraProbability_le (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) (A : Finset (Fin k)) {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
    (hlo : ∀ j g, (1/2 : ℝ)*FiniteLaw.uniform _ g ≤ lineLaw (G.bits j) z hz hz' g)
    (hhi : ∀ j g, lineLaw (G.bits j) z hz hz' g ≤ 2*FiniteLaw.uniform _ g) :
    (G.size : ℝ)^A.card * H.extraProbability x y A (fun j => lineLaw (G.bits j) z hz hz') ≤
      Real.exp ((G.b : ℝ)*(h+k) + Real.log 4*k*G.b) := by
…

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw

  23. theorem OAI.CoordinateSweeps.Grid.Holes.scaled_placementKernel_abs_le line 406

    Source comment

    Source 04:eq8, with an explicit absolute constant in place of O(·). Only valid input placements are needed; impossible output events contribute zero.
    theorem scaled_placementKernel_abs_le (H : G.Holes h) (x y : Fin k → G.Slot)
    (hx : H.ValidInput x) {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
    (hlo : ∀ j g, (1/2 : ℝ)*FiniteLaw.uniform _ g ≤ lineLaw (G.bits j) z hz hz' g)
    (hhi : ∀ j g, lineLaw (G.bits j) z hz hz' g ≤ 2*FiniteLaw.uniform _ g) :
    |(G.size : ℝ)^k * H.placementKernel x y (fun j => lineLaw (G.bits j) z hz hz')| ≤
      (2 : ℝ)^k * Real.exp ((G.b : ℝ)*(h+k) + Real.log 4*k*G.b) := by
…

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw

  24. def OAI.CoordinateSweeps.Grid.Holes.ValidOutput line 441
  25. def OAI.CoordinateSweeps.Grid.Holes.placementHSsq line 445

    Source comment

    Counting-measure Hilbert--Schmidt square on the actual free placements.
    def placementHSsq (H : G.Holes h)
    (μ : ∀ j, FiniteLaw (Equiv.Perm (Cube (G.bits j)))) : ℝ :=
…

    Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube

  26. theorem OAI.CoordinateSweeps.Grid.Holes.endpoint_productMass line 451

    Source comment

    The full endpoint product weight is exactly s^(-2k).
    theorem endpoint_productMass (p : Fin k → G.Slot × G.Slot) :
    Coverage.productMass G.endpointWeight p = (G.size : ℝ)⁻¹^(2*k) := by
…

    Mentions: OAI.CoordinateSweeps.Coverage.productMass

  27. theorem OAI.CoordinateSweeps.Grid.Holes.placementHSsq_eq_full line 458

    Source comment

    Rewriting the counting norm using independent full-grid endpoints never conditions the auxiliary trajectories on being valid placements.
    theorem placementHSsq_eq_full (H : G.Holes h)
    (μ : ∀ j, FiniteLaw (Equiv.Perm (Cube (G.bits j)))) :
    H.placementHSsq (k := k) μ =
…

    Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube

  28. theorem OAI.CoordinateSweeps.Grid.Holes.placementHSsq_le line 497

    Source comment

    Source 04:eqs8--9 combined, with an explicit counting HS estimate. This is the direct, unweakened many-coordinate sparse-kernel estimate.
    theorem placementHSsq_le (H : G.Holes h) (hH : H.Feasible)
    {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
    (hlo : ∀ j g, (1/2 : ℝ)*FiniteLaw.uniform _ g ≤ lineLaw (G.bits j) z hz hz' g)
    (hhi : ∀ j g, lineLaw (G.bits j) z hz hz' g ≤ 2*FiniteLaw.uniform _ g)
    (hsmall : ((k+h : ℕ) : ℝ)*G.lineSharingRate ≤ 1) :
    H.placementHSsq (k := k) (fun j => lineLaw (G.bits j) z hz hz') ≤
…

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw