AdviceImageLaw.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

The exact visible-advice law for a fixed latent map

For every fixed binary-linear map A, including rank-deficient maps, a uniform latent column has a uniform image in range A. An explicit range/kernel bijection proves the assertion simultaneously for every intercept and slope. The final theorem starts with the actual pair of independently uniform linear maps on the partner answer space and pushes it to independent uniform visible coefficients in W × range A. No full-rank or independence premise is assumed.

def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.rangePoint line 35
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.selectedLift line 38
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.selectedLift_spec line 41
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.rangePoint_lift_add_kernel line 45
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.imageKernelEquiv line 52
Source documentation
Every range fibre is one translate of the same kernel.
```
def imageKernelEquiv (A : K →ₗ[F2] S) : K ≃ A.range × A.ker where
…
```
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.columnImage line 71
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.columnSplitEquiv line 74
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.visibleCoefficients line 78
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.coefficientsSplitEquiv line 82
instance OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.rangeFintype line 87
instance OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.kernelFintype line 90
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.uniform_visible_coefficients line 95
Source documentation
Exact pushforward law for all columns jointly, including the original intercept. This implies every event identity, not just individual marginals.
```
theorem uniform_visible_coefficients {I : Type} [Fintype I] [DecidableEq I]
    [Fintype W] [Fintype K] [Fintype S]
    (A : K →ₗ[F2] S) (F : (I → W × A.range) → ℝ) :
    (𝔼 columns : I → W × K, F (visibleCoefficients A columns)) =
      𝔼 visible : I → W × A.range, F visible := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.visibleCoefficients

theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.uniform_coordinate_product line 110

Source documentation

The full product law exposes mutual independence of every raw coefficient.

theorem uniform_coordinate_product {I E : Type} [Fintype I] [DecidableEq I] [Fintype E]
    (f : I → E → ℝ) :
    (𝔼 columns : I → E, ∏ i, f i (columns i)) = ∏ i, 𝔼 e : E, f i e := by
…

theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.visible_coefficient_product line 118
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.uniform_pushforward_of_expect line 126
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.visible_coefficients_pushforward line 144
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.visible_card_le line 151
Source documentation
The worst-case codomain cardinality suffices; no rank estimate is needed.
```
theorem visible_card_le [Fintype W] [Fintype K] [Fintype S] (A : K →ₗ[F2] S) :
    Fintype.card (W × A.range) ≤ Fintype.card W * Fintype.card S := by
…
```
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.visible_card_binary_le line 157
abbrev OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.PartnerSpace line 172
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.coefficients_comp line 175
Source documentation
Raw coefficients commute with actual linear-map composition.
```
theorem coefficients_comp (A : K →ₗ[F2] S) (M : PartnerSpace rhs J →ₗ[F2] K) :
    coefficients rhs J S (A.comp M) = fun i => A (coefficients rhs J K M i) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.PartnerSpace
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actualVisibleCoefficients line 180
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actualVisibleCoefficients_second line 186
Source documentation
The displayed second component is precisely the coefficient of S = A M.
```
theorem actualVisibleCoefficients_second (A : K →ₗ[F2] S)
    (T : PartnerSpace rhs J →ₗ[F2] W) (M : PartnerSpace rhs J →ₗ[F2] K)
    (i : RawSlot J) :
    ((actualVisibleCoefficients rhs J A (T, M) i).2 : S) =
      coefficients rhs J S (A.comp M) i := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.PartnerSpace, OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actualVisibleCoefficients
def OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actualMapPairEquiv line 194
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actual_maps_visible_uniform line 202
Source documentation
Sampling the actual independent maps T and M yields the claimed joint uniform coefficient law of (T,A M), for every fixed equation tuple and mask.
```
theorem actual_maps_visible_uniform [Fintype W] [Fintype K] [Fintype S]
    (A : K →ₗ[F2] S) (F : (RawSlot J → W × A.range) → ℝ) :
    (𝔼 maps : (PartnerSpace rhs J →ₗ[F2] W) × (PartnerSpace rhs J →ₗ[F2] K),
        F (actualVisibleCoefficients rhs J A maps)) =
      𝔼 gamma : RawSlot J → W × A.range, F gamma := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.PartnerSpace, OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actualVisibleCoefficients
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actual_maps_visible_product line 214
theorem OAI.UniqueGamesTheorem.Clean.AdviceImageLaw.actual_maps_visible_pushforward line 222