OAI/Probability/CoordinateSweeps/SparseDimension.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoordinateSweeps.Grid.Holes.inputPlacementEquiv line 34
  2. def OAI.CoordinateSweeps.Grid.Holes.outputFreePlacementEquiv line 40
  3. def OAI.CoordinateSweeps.Grid.Holes.outputPlacementEquiv line 46
  4. lemma OAI.CoordinateSweeps.Grid.Holes.outputPlacementEquiv_apply line 50
  5. def OAI.CoordinateSweeps.Grid.Holes.residualFree line 53
  6. lemma OAI.CoordinateSweeps.Grid.Holes.residualFree_apply line 56
  7. lemma OAI.CoordinateSweeps.Grid.Holes.endpointEvent_residualFree line 59
  8. lemma OAI.CoordinateSweeps.Grid.Holes.extraProbability_eq_residual_sum line 78
  9. def OAI.CoordinateSweeps.Grid.Holes.referencePartial line 114

    Source comment

    Partial endpoint matrix written on a single placement set using the reference sweep; every variable is a literal conditional path probability.
    def referencePartial (hf : H.Feasible) (μ : ∀ j, FiniteLaw (Equiv.Perm (Cube (G.bits j))))
    (A : Finset (Fin k)) (x y : Fin k ↪ H.FreeAt 0) : ℝ :=
…

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

  10. lemma OAI.CoordinateSweeps.Grid.Holes.referencePartial_depends line 118
  11. lemma OAI.CoordinateSweeps.Grid.Holes.referencePartial_full line 127
  12. lemma OAI.CoordinateSweeps.Grid.Holes.referenceAlternating_entry line 140
  13. lemma OAI.CoordinateSweeps.Grid.Holes.referenceAlternating_hs line 146
  14. theorem OAI.CoordinateSweeps.Grid.Holes.conditional_norm_le_placementHS line 159

    Source comment

    The missing attachment of source04:eq7 to the faithful conditional irreducible average, not merely an abstract stochastic matrix.
    theorem conditional_norm_le_placementHS (hf : H.Feasible) {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
    (ρ : UnitaryIrrep (Equiv.Perm (H.FreeAt 0)))
    (u : Fin ρ.dimension → ℂ) (hu : u ≠ 0) (x₀ : Fin k ↪ H.FreeAt 0)
    (hfixed : ∀ g : Equiv.Perm (H.FreeAt 0), (∀ i, g (x₀ i)=x₀ i) → ρ.asRepresentation g u=u)
    (hnof : ∀ A : Finset (H.FreeAt 0), A.card < k → ∀ v : Fin ρ.dimension → ℂ,
      (∀ g : Equiv.Perm (H.FreeAt 0), (∀ a ∈ A, g a=a) → ρ.asRepresentation g v=v) → v=0) :
    ‖H.conditionalAverage hf z (ρ.pullback H.stabilizerFreeEquiv)‖ ≤
      Real.sqrt (H.placementHSsq (k := k) (fun j => lineLaw (G.bits j) z hz hz')) := by
…

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.lineLaw

  15. def OAI.CoordinateSweeps.realSign line 195

    Source comment

    Archived complete binary-sign support, reused without a new-result claim. The real-valued sign character, not a replacement for the permutation.
    def realSign {Ω : Type*} [Fintype Ω] [DecidableEq Ω] : Equiv.Perm Ω →* ℝ where
…
  16. def OAI.CoordinateSweeps.boolSwitch line 200
  17. theorem OAI.CoordinateSweeps.boolSwitch_apply line 203
  18. theorem OAI.CoordinateSweeps.sign_boolSwitch line 206
  19. theorem OAI.CoordinateSweeps.pairSwitch_eq_prod line 209
  20. theorem OAI.CoordinateSweeps.sign_pairSwitch line 216
  21. theorem OAI.CoordinateSweeps.sign_binaryLayer line 227
  22. theorem OAI.CoordinateSweeps.sum_sign_pairSwitch line 234
  23. theorem OAI.CoordinateSweeps.sign_binarySweep line 240
  24. theorem OAI.CoordinateSweeps.sum_sign_binarySweep line 246
  25. lemma OAI.CoordinateSweeps.signed_sum_zero_of_swap line 271
  26. lemma OAI.CoordinateSweeps.sum_uniform_realSign line 293
  27. lemma OAI.CoordinateSweeps.sum_map_mul line 300
  28. lemma OAI.CoordinateSweeps.sum_binary_realSign line 308
  29. lemma OAI.CoordinateSweeps.sum_lineLaw_realSign line 313
  30. lemma OAI.CoordinateSweeps.uniform_signed_assignments_zero line 320
  31. lemma OAI.CoordinateSweeps.Grid.realSign_fiberPerm line 335
  32. lemma OAI.CoordinateSweeps.Grid.realSign_stage line 345
  33. lemma OAI.CoordinateSweeps.Grid.realSign_sweep line 353
  34. lemma OAI.CoordinateSweeps.Grid.signed_line_factorization line 362
  35. def OAI.CoordinateSweeps.Grid.Holes.jointLineEvent line 385
  36. lemma OAI.CoordinateSweeps.Grid.Holes.signed_endpoint_factorization line 389
  37. lemma OAI.CoordinateSweeps.Grid.Holes.signed_endpoint_zero_of_unused line 402
  38. lemma OAI.CoordinateSweeps.Grid.Holes.exists_unused_line line 422
  39. theorem OAI.CoordinateSweeps.Grid.Holes.signed_endpoint_zero_many line 441

    Source comment

    Literal many-coordinate column cancellation; no complex conditioning.
    theorem signed_endpoint_zero_many (x y : Fin k → G.Slot) {z : ℝ}
    (hz : 0 ≤ z) (hz' : z ≤ 1) (j : Fin G.b) (hj : 0 < G.bits j)
    (hsize : h+k < Fintype.card (G.Line j)) :
    (∑ ω : G.Choices, if H.Compatible ω ∧ G.endpointEvent x y Finset.univ ω then
      G.choiceWeight z ω*realSign (G.sweep ω) else 0)=0 := by
…

    Mentions: OAI.CoordinateSweeps.realSign

  40. lemma OAI.CoordinateSweeps.exists_two_unassigned line 453

    Source comment

    More than one unassigned slot per line on average forces two free slots on a common line. Assignments need not be injective for this counting step.
    lemma exists_two_unassigned {I U V : Type*} [Fintype I] [Fintype U] [Fintype V]
    [DecidableEq U] [DecidableEq V] (f : I → U × V)
    (hh : Fintype.card I+Fintype.card V < Fintype.card (U × V)) :
    ∃ a b : U, ∃ v : V, a ≠ b ∧ (∀ i, f i ≠ (a,v)) ∧ ∀ i, f i ≠ (b,v) := by
…

    Mentions: OAI.CoordinateSweeps.a

  41. lemma OAI.CoordinateSweeps.Grid.Holes.uniform_signed_joint_zero line 488
  42. theorem OAI.CoordinateSweeps.Grid.Holes.signed_endpoint_zero_uniform line 524

    Source comment

    Exact zero at the real uniform law, including bounded coordinate counts.
    theorem signed_endpoint_zero_uniform (x y : Fin k → G.Slot) (j : Fin G.b)
    (hsize : h+k+Fintype.card (G.Line j) < G.size) :
    (∑ ω : G.Choices, if H.Compatible ω ∧ G.endpointEvent x y Finset.univ ω then
      G.choiceWeight 0 ω*realSign (G.sweep ω) else 0)=0 := by
…

    Mentions: OAI.CoordinateSweeps.realSign

  43. def OAI.CoordinateSweeps.UnitaryIrrep.signTwist line 558
  44. lemma OAI.CoordinateSweeps.UnitaryIrrep.signTwist_rep line 575
  45. theorem OAI.CoordinateSweeps.PlacementOccurrence.average_zero_of_placement_zero line 591
  46. lemma OAI.CoordinateSweeps.Grid.Holes.realSign_freePerm line 617
  47. lemma OAI.CoordinateSweeps.Grid.Holes.realSign_residualFree line 632
  48. lemma OAI.CoordinateSweeps.Grid.Holes.signed_reference_entry_zero line 638
  49. theorem OAI.CoordinateSweeps.Grid.Holes.conditional_zero_of_signed_endpoints line 681

    Source comment

    Column cancellation is now on the faithful conditional average, not just on raw signed endpoint numerators.
    theorem conditional_zero_of_signed_endpoints (hf : H.Feasible) (z : ℝ)
    (ρ : UnitaryIrrep (Equiv.Perm (H.FreeAt 0)))
    (u : Fin ρ.dimension → ℂ) (hu : u ≠ 0) (x₀ : Fin k ↪ H.FreeAt 0)
    (hfixed : ∀ g : Equiv.Perm (H.FreeAt 0), (∀ i, g (x₀ i)=x₀ i) →
      (SparseDimension.signTwist ρ.asRepresentation) g u=u)
    (hzero : ∀ x y : Fin k → G.Slot,
      (∑ ω : G.Choices, if H.Compatible ω ∧ G.endpointEvent x y Finset.univ ω then
        G.choiceWeight z ω*realSign (G.sweep ω) else 0)=0) :
    H.conditionalAverage hf z (ρ.pullback H.stabilizerFreeEquiv)=0 := by
…

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SparseDimension.signTwist, OAI.CoordinateSweeps.realSign

  50. theorem OAI.CoordinateSweeps.Grid.Holes.conditional_column_zero_many line 728
  51. theorem OAI.CoordinateSweeps.Grid.Holes.conditional_column_zero_uniform line 737