Concatenation.lean`

49 declarations, 0 contain sorry, 0 declared as axioms

Common-parent factorization before fresh orientation

This is the linear algebra in the lift-factorization lemma of v2 Section 2. The map gamma is obtained from the whole parent family and the first aggregate coordinate. It is chosen once, before any child is selected. No rank, genericity, or independence assumption is needed for this step.

def OAI.MaxCutGames.Gadget.aggregate line 21
Source documentation
Sum of the oriented block inclusions on the child logical symbols.
```
def aggregate (J : I → B →ₗ[k] X × B) : (I → B) →ₗ[k] X × B where
…
```
def OAI.MaxCutGames.Gadget.shiftAggregate line 27
Source documentation
The same aggregate, evaluated on actual child shifts.
```
def shiftAggregate (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B) :
    (I → R) →ₗ[k] X × B where
…
```
def OAI.MaxCutGames.Gadget.parentShifts line 35
Source documentation
The parent shift space: precisely the child shifts with zero first aggregate coordinate.
```
def parentShifts (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B) :
    Submodule k (I → R) :=
…
```
def OAI.MaxCutGames.Gadget.parentLogical line 40
Source documentation
Parent logical translation, the second aggregate coordinate.
```
def parentLogical (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B) :
    parentShifts J lam →ₗ[k] B :=
…
```
Mentions: OAI.MaxCutGames.Gadget.parentShifts
def OAI.MaxCutGames.Gadget.parentEmbed line 46
Source documentation
Embedding parent shifts in the actual product of child input spaces.
```
def parentEmbed (J : I → B →ₗ[k] X × B) (lam : R →ₗ[k] B)
    (e : R →ₗ[k] P) : parentShifts J lam →ₗ[k] (I → P) where
…
```
Mentions: OAI.MaxCutGames.Gadget.parentShifts
theorem OAI.MaxCutGames.Gadget.parentEmbed_injective line 52
theorem OAI.MaxCutGames.Gadget.shiftAggregate_surjective line 60
theorem OAI.MaxCutGames.Gadget.parentLogical_surjective line 72
def OAI.MaxCutGames.Gadget.parentOutput line 84

theorem OAI.MaxCutGames.Gadget.aggregate_output_shift line 90

Source documentation

Child equivariance gives the actual aggregate translation formula.

theorem aggregate_output_shift (J : I → B →ₗ[k] X × B)
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (C : P → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h)
    (u : I → P) (h : I → R) :
    aggregate J (fun i => C (u i + e (h i))) =
      aggregate J (fun i => C (u i)) + shiftAggregate J lam h := by
…

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.shiftAggregate

theorem OAI.MaxCutGames.Gadget.parentOutput_equivariant line 101

Source documentation

Parent equivariance is derived for the kernel-defined shift space.

theorem parentOutput_equivariant (J : I → B →ₗ[k] X × B)
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (C : P → B) (Q : X → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h)
    (u : I → P) (h : parentShifts J lam) :
    parentOutput J C Q (u + parentEmbed J lam e h) =
      parentOutput J C Q u + parentLogical J lam h := by
…

Mentions: OAI.MaxCutGames.Gadget.parentShifts, OAI.MaxCutGames.Gadget.parentOutput, OAI.MaxCutGames.Gadget.parentEmbed, OAI.MaxCutGames.Gadget.parentLogical

theorem OAI.MaxCutGames.Gadget.output_difference_shift line 123
Source documentation
The output difference at a fixed perturbation is invariant under logical shifts. This is the conditioning input for the exact nonlinear noise law.
```
theorem output_difference_shift
    (C : P → B) (e : R → P) (lam : R → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h) (u a : P) (h : R) :
    C (u + e h + a) - C (u + e h) = C (u + a) - C u := by
…
```
structure OAI.MaxCutGames.Gadget.Stage line 138
Source documentation
An equivariant finite stage, including its concrete finite noise sampler.
```
structure Stage (k : Type u) (B : Type v) [CommRing k]
    [AddCommGroup B] [Module k B] where
…
```
def OAI.MaxCutGames.Gadget.Stage.base line 168
Source documentation
The height-zero input, shift and uniform noise alphabet.
```
def base : Stage k B where
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage
def OAI.MaxCutGames.Gadget.Stage.next line 184
Source documentation
One complete recursive level, with actual single-coordinate leaf noise.
```
noncomputable def next (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B)
    (s : Stage k B) : Stage k B where
…
```
Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.Stage
def OAI.MaxCutGames.Gadget.Stage.iterate line 201
Source documentation
The finite stage at any natural height, using the same alphabet and block family at every level. Surjectivity and equivariance have been proved by the constructor, and hence are available at every height without extra hypotheses.
```
noncomputable def iterate (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (Q : X → B) : ℕ → Stage k B
  | 0 => base
  | n + 1 => next J hJ Q (iterate J hJ Q n)
```
Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.Stage.base, OAI.MaxCutGames.Gadget.Stage.next
theorem OAI.MaxCutGames.Gadget.Stage.iterate_zero line 206
theorem OAI.MaxCutGames.Gadget.Stage.iterate_succ line 210
theorem OAI.MaxCutGames.Gadget.family_factors_of_ker line 238
Source documentation
A linear family vanishing on the kernel of a surjection factors as one linear family on the target. In particular the factor is linear in its character parameter, rather than a separate arbitrary choice for each one.
```
theorem family_factors_of_ker
    (f : T →ₗ[k] X) (hf : Function.Surjective f)
    (ψ : S →ₗ[k] (T →ₗ[k] k))
    (hker : ∀ z t, f t = 0 → ψ z t = 0) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k), ∀ z t, ψ z t = γ z (f t) := by
…
```
theorem OAI.MaxCutGames.Gadget.common_parent_factorization line 259
Source documentation
The common first-coordinate character of a parent lift. ψ z is the parent character on child shifts, ζ z its prescribed logical character, and (a,b) the aggregate. A parent shift is exactly a tuple with a=0. The conclusion quantifies one γ before all tuples and all later children.
```
theorem common_parent_factorization
    (a : T →ₗ[k] X) (b : T →ₗ[k] B) (ha : Function.Surjective a)
    (ψ : S →ₗ[k] (T →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z t, a t = 0 → ψ z t = ζ z (b t)) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k),
      ∀ z t, ψ z t = γ z (a t) + ζ z (b t) := by
…
```

theorem OAI.MaxCutGames.Gadget.common_child_factorization line 281

Source documentation

Evaluating the single parent factor on any child embedding gives the child restriction formula. The same γ works for every child, so its choice cannot depend on the fresh orientation subsequently sampled at that child.

theorem common_child_factorization
    {ι P : Type*} [AddCommGroup P] [Module k P]
    (a : T →ₗ[k] X) (b : T →ₗ[k] B) (ha : Function.Surjective a)
    (ψ : S →ₗ[k] (T →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z t, a t = 0 → ψ z t = ζ z (b t))
    (child : ι → P →ₗ[k] T) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k),
      ∀ i z p, ψ z (child i p) = γ z (a (child i p)) + ζ z (b (child i p)) := by
…

theorem OAI.MaxCutGames.Gadget.aggregate_fst_surjective line 293

Source documentation

For a surjective aggregate, its first coordinate is surjective.

theorem aggregate_fst_surjective (A : T →ₗ[k] X × B)
    (hA : Function.Surjective A) :
    Function.Surjective ((LinearMap.fst k X B).comp A) := by
…

def OAI.MaxCutGames.Gadget.tupleEmbed line 322
Source documentation
Inclusion of all child shifts before imposing the parent kernel condition.
```
def tupleEmbed (e : R →ₗ[k] P) : (I → R) →ₗ[k] (I → P) where
…
```
theorem OAI.MaxCutGames.Gadget.tupleEmbed_single line 328
theorem OAI.MaxCutGames.Gadget.shiftAggregate_single line 335

theorem OAI.MaxCutGames.Gadget.parent_lift_common_child line 344

Source documentation

Actual parent lifts factor through the same aggregate first-coordinate family on all child shifts. The existential γ occurs before both i and h. This is the common-parent requirement used before revealing fresh orientation.

theorem parent_lift_common_child
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (hlam : Function.Surjective lam)
    (ψ : S →ₗ[k] ((I → P) →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z (h : parentShifts J lam),
      ψ z (parentEmbed J lam e h) = ζ z (parentLogical J lam h)) :
    ∃ γ : S →ₗ[k] (X →ₗ[k] k), ∀ i z h,
      ψ z (Pi.single i (e h)) =
        γ z (J i (lam h)).1 + ζ z (J i (lam h)).2 := by
…

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.parentShifts, OAI.MaxCutGames.Gadget.parentEmbed, OAI.MaxCutGames.Gadget.parentLogical

theorem OAI.MaxCutGames.Gadget.parent_lift_child_kernel line 373

Source documentation

In particular, every child restriction annihilates the child's logical kernel. This proves that a child logical character exists for every lift.

theorem parent_lift_child_kernel
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (hlam : Function.Surjective lam)
    (ψ : S →ₗ[k] ((I → P) →ₗ[k] k)) (ζ : S →ₗ[k] (B →ₗ[k] k))
    (hlift : ∀ z (h : parentShifts J lam),
      ψ z (parentEmbed J lam e h) = ζ z (parentLogical J lam h))
    (i : I) (z : S) (h : R) (hh : lam h = 0) :
    ψ z (Pi.single i (e h)) = 0 := by
…

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.parentShifts, OAI.MaxCutGames.Gadget.parentEmbed, OAI.MaxCutGames.Gadget.parentLogical

structure OAI.MaxCutGames.Gadget.Lift line 401
Source documentation
A linear lift of a logical character subspace to the actual stage input.
```
structure Lift (s : Stage k B) (S : Submodule k (B →ₗ[k] k)) where
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage
def OAI.MaxCutGames.Gadget.Lift.restrict line 406
Source documentation
Restricting a lift preserves its prescribed logical characters.
```
def Lift.restrict {s : Stage k B} {S T : Submodule k (B →ₗ[k] k)}
    (L : Lift s T) (hST : S ≤ T) : Lift s S where
…
```
Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.Lift
def OAI.MaxCutGames.Gadget.singleInput line 415
Source documentation
Linear insertion into one physical input coordinate.
```
def singleInput (i : I) (P : Type v) [AddCommGroup P] [Module k P] :
    P →ₗ[k] (I → P) where
…
```
def OAI.MaxCutGames.Gadget.childCharacter line 423
Source documentation
The logical map of a child, obtained from the common parent first-coordinate map and the prescribed logical character.
```
def childCharacter (J : I → B →ₗ[k] X × B)
    {S : Submodule k (B →ₗ[k] k)} (γ : S →ₗ[k] (X →ₗ[k] k)) (i : I) :
    S →ₗ[k] (B →ₗ[k] k) where
…
```
theorem OAI.MaxCutGames.Gadget.exists_common_child_character line 432

def OAI.MaxCutGames.Gadget.descendantFamily line 449

Source documentation

The descendant family using a section of the actual image.

def descendantFamily {s : Stage k B} {S : Submodule k (B →ₗ[k] k)}
    (ψ : S →ₗ[k] ((I → s.Input) →ₗ[k] k)) (i : I)
    (φ : S →ₗ[k] (B →ₗ[k] k))
    (sectionMap : LinearMap.range φ →ₗ[k] S) :
    LinearMap.range φ →ₗ[k] (s.Input →ₗ[k] k) where
…

Mentions: OAI.MaxCutGames.Gadget.Stage

theorem OAI.MaxCutGames.Gadget.exists_descendant_lift line 461

Source documentation

Every child image carries a genuine child lift. The section is constructed by ordinary linear algebra and is chosen without any later path or leaf symbol.

theorem exists_descendant_lift
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (Q : X → B) (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
    (L : Lift (Stage.next J hJ Q s) S)
    (γ : S →ₗ[k] (X →ₗ[k] k))
    (hγ : ∀ i z h, L.family z (Pi.single i (s.embed h)) =
      childCharacter J γ i z (s.logical h)) (i : I) :
    ∃ (L' : Lift s (LinearMap.range (childCharacter J γ i)))
      (sectionMap : LinearMap.range (childCharacter J γ i) →ₗ[k] S),
      (∀ z, childCharacter J γ i (sectionMap z) = z.val) ∧
      (∀ z p, L'.family z p = L.family (sectionMap z) (Pi.single i p)) := by
…

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.next, OAI.MaxCutGames.Gadget.childCharacter

theorem OAI.MaxCutGames.Gadget.descendant_detection_implies_parent line 491

Source documentation

Pointwise containment of child detection in parent detection. Repeating this implication along a path preserves the original family at the root.

theorem descendant_detection_implies_parent
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (Q : X → B) (s : Stage k B) (S : Submodule k (B →ₗ[k] k))
    (L : Lift (Stage.next J hJ Q s) S)
    {S' : Submodule k (B →ₗ[k] k)} (L' : Lift s S')
    (sectionMap : S' →ₗ[k] S) (i : I)
    (hfamily : ∀ z p, L'.family z p = L.family (sectionMap z) (Pi.single i p))
    (n : s.Noise) (hdetect : ∃ z, L'.family z (s.noise n) ≠ 0) :
    ∃ z, L.family z ((Stage.next J hJ Q s).noise (i, n)) ≠ 0 := by
…

Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.Stage.next

theorem OAI.MaxCutGames.Gadget.Orientation.sum_action_eq line 529
Source documentation
Right translation of the uniform group element changes the starting point, but leaves the complete sample sum unchanged.
```
theorem sum_action_eq (x y : X) (h : ∃ a : G, a • x = y) (f : X → ℚ) :
    (∑ g : G, f (g • x)) = ∑ g : G, f (g • y) := by
…
```
theorem OAI.MaxCutGames.Gadget.Orientation.card_mul_sum_action line 537
Source documentation
Cross-multiplied uniform-pushforward identity for a transitive finite action. This form also handles empty event sets without additional cases.
```
theorem card_mul_sum_action (x : X)
    (transitive : ∀ y : X, ∃ a : G, a • x = y) (f : X → ℚ) :
    (Fintype.card X : ℚ) * (∑ g : G, f (g • x)) =
      (Fintype.card G : ℚ) * (∑ y : X, f y) := by
…
```
theorem OAI.MaxCutGames.Gadget.Orientation.mean_action line 557
Source documentation
A uniform group element sends a fixed point to the uniform distribution on the entire transitive space. Apply to indicator functions for event bounds.
```
theorem mean_action (x : X)
    (transitive : ∀ y : X, ∃ a : G, a • x = y) (f : X → ℚ) :
    (∑ g : G, f (g • x)) / Fintype.card G =
      (∑ y : X, f y) / Fintype.card X := by
…
```
theorem OAI.MaxCutGames.Gadget.Orientation.exists_map_eq_of_finrank_eq line 575
Source documentation
Every two equal-dimensional subspaces are related by an automorphism of the ambient space. This supplies actual transitivity, rather than assuming the desired distribution on the Grassmannian.
```
theorem exists_map_eq_of_finrank_eq (E F : Submodule K V)
    (h : finrank K E = finrank K F) :
    ∃ a : V ≃ₗ[K] V, E.map a.toLinearMap = F := by
…
```
theorem OAI.MaxCutGames.Gadget.Orientation.rank_map line 592
Source documentation
Rank does not depend on the fresh orientation.
```
theorem rank_map (E : Submodule K V) (a : V ≃ₗ[K] V) :
    finrank K (E.map a.toLinearMap) = finrank K E :=
…
```
def OAI.MaxCutGames.Gadget.Orientation.RankSpace line 597
Source documentation
The finite Grassmannian at a rank chosen before orientation.
```
def RankSpace (K V : Type*) [Field K] [AddCommGroup V] [Module K V] (r : ℕ) :=
…
```
instance OAI.MaxCutGames.Gadget.Orientation.rankSpaceAction line 600
theorem OAI.MaxCutGames.Gadget.Orientation.rankSpace_transitive line 610
Source documentation
Equal-rank transitivity specialized to the rank-indexed sampling space.
```
theorem rankSpace_transitive {r : ℕ} (E F : RankSpace K V r) :
    ∃ a : V ≃ₗ[K] V, a • E = F := by
…
```
Mentions: OAI.MaxCutGames.Gadget.Orientation.RankSpace

theorem OAI.MaxCutGames.Gadget.Orientation.mean_oriented_subspace line 618

Source documentation

The exact uniform law of a fixed-rank subspace under a fresh uniform linear orientation, with no genericity or independence premise.

theorem mean_oriented_subspace {r : ℕ} [Fintype (V ≃ₗ[K] V)]
    [Fintype (RankSpace K V r)] (E : RankSpace K V r) (f : RankSpace K V r → ℚ) :
    (∑ a : V ≃ₗ[K] V, f (a • E)) / Fintype.card (V ≃ₗ[K] V) =
      (∑ F : RankSpace K V r, f F) / Fintype.card (RankSpace K V r) :=
…

Mentions: OAI.MaxCutGames.Gadget.Orientation.RankSpace

theorem OAI.MaxCutGames.Gadget.Orientation.rank_dual_pullback line 629
Source documentation
Pullback of a fixed character space by an isomorphism preserves rank. The character space is an argument preceding the newly chosen orientation.
```
theorem rank_dual_pullback (E : Submodule K (Module.Dual K U)) (J : B ≃ₗ[K] U) :
    finrank K (E.map J.dualMap.toLinearMap) = finrank K E :=
…
```
def OAI.MaxCutGames.Gadget.Orientation.orientationEquiv line 635
Source documentation
Choosing a reference isomorphism identifies all orientations with the automorphism group of the target.
```
def orientationEquiv (J₀ : B ≃ₗ[K] U) : (B ≃ₗ[K] U) ≃ (U ≃ₗ[K] U) where
…
```

theorem OAI.MaxCutGames.Gadget.Orientation.mean_map_equiv line 643

Source documentation

Uniform orientations between two spaces send a fixed character subspace to the uniform distribution on all subspaces of the same dimension.

theorem mean_map_equiv [FiniteDimensional K U] (E : Submodule K B) (J₀ : B ≃ₗ[K] U)
    [Fintype (B ≃ₗ[K] U)] [Fintype (U ≃ₗ[K] U)]
    [Fintype (RankSpace K U (finrank K E))]
    (f : RankSpace K U (finrank K E) → ℚ) :
    (∑ J : B ≃ₗ[K] U, f ⟨E.map J.toLinearMap, J.finrank_map_eq E⟩) /
        Fintype.card (B ≃ₗ[K] U) =
      (∑ F : RankSpace K U (finrank K E), f F) /
        Fintype.card (RankSpace K U (finrank K E)) := by
…

Mentions: OAI.MaxCutGames.Gadget.Orientation.RankSpace

def OAI.MaxCutGames.Gadget.Orientation.dualOrientationEquiv line 670
Source documentation
Dualization is a bijection on finite-dimensional isomorphisms. This connects uniform primal orientations to uniform character-space orientations.
```
def dualOrientationEquiv [FiniteDimensional K B] [FiniteDimensional K U] :
    (B ≃ₗ[K] U) ≃ (Module.Dual K U ≃ₗ[K] Module.Dual K B) where
…
```
theorem OAI.MaxCutGames.Gadget.Orientation.mean_dual_pullback line 683