AdviceFibers.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Exact visible row advice and private matrix coordinates

Every nonempty fiber of M ↦ A ∘ M is an affine copy of Hom(E, ker A), whether or not A is surjective. Choosing one base matrix for each attainable row gives a product decomposition of the complete matrix space. Uniform sampling therefore makes visible row advice and the hidden kernel-valued matrix independent.

abbrev OAI.MaxCutGames.Decoder.AdviceFibers.RowFiber line 28
Source documentation
Actual matrices with the specified observed row advice.
```
abbrev RowFiber (A : K →ₗ[F2] R) (S : E →ₗ[F2] R) :=
…
```
def OAI.MaxCutGames.Decoder.AdviceFibers.kernelDifference line 32
Source documentation
Hidden coordinates relative to one base matrix in the same row fiber.
```
def kernelDifference (A : K →ₗ[F2] R) (S : E →ₗ[F2] R)
    (M₀ : E →ₗ[F2] K) (h₀ : A.comp M₀ = S) (M : RowFiber A S) :
    E →ₗ[F2] A.ker :=
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.RowFiber
theorem OAI.MaxCutGames.Decoder.AdviceFibers.kernelDifference_apply line 45
def OAI.MaxCutGames.Decoder.AdviceFibers.assemble line 50
Source documentation
Reassemble an actual matrix from its fixed visible base and private part.
```
def assemble (A : K →ₗ[F2] R) (M₀ : E →ₗ[F2] K)
    (N : E →ₗ[F2] A.ker) : E →ₗ[F2] K :=
…
```
theorem OAI.MaxCutGames.Decoder.AdviceFibers.assemble_apply line 54
theorem OAI.MaxCutGames.Decoder.AdviceFibers.observed_assemble line 59
Source documentation
Observed advice is completely unchanged by the private coordinates.
```
theorem observed_assemble (A : K →ₗ[F2] R) (M₀ : E →ₗ[F2] K)
    (N : E →ₗ[F2] A.ker) : A.comp (assemble A M₀ N) = A.comp M₀ := by
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.assemble
def OAI.MaxCutGames.Decoder.AdviceFibers.rowFiberEquiv line 66
Source documentation
The exact row-fiber bijection; no rank or surjectivity premise is needed.
```
def rowFiberEquiv (A : K →ₗ[F2] R) (S : E →ₗ[F2] R)
    (M₀ : E →ₗ[F2] K) (h₀ : A.comp M₀ = S) :
    (E →ₗ[F2] A.ker) ≃ RowFiber A S where
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.RowFiber
theorem OAI.MaxCutGames.Decoder.AdviceFibers.rowFiberEquiv_coe line 83
theorem OAI.MaxCutGames.Decoder.AdviceFibers.rowFiberEquiv_symm line 87
theorem OAI.MaxCutGames.Decoder.AdviceFibers.assemble_affine_target line 92
Source documentation
Affine target intercepts are retained in the private coordinates.
```
theorem assemble_affine_target (A : K →ₗ[F2] R) (M₀ : E →ₗ[F2] K)
    (N : E →ₗ[F2] A.ker) (z : E) (u : K) :
    assemble A M₀ N z + u = (N z : K) + (M₀ z + u) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.assemble
theorem OAI.MaxCutGames.Decoder.AdviceFibers.rowFiber_card line 104
theorem OAI.MaxCutGames.Decoder.AdviceFibers.rowFiber_expect line 110
Source documentation
Uniform private matrices push forward to uniform matrices in the fiber.
```
theorem rowFiber_expect (M₀ : E →ₗ[F2] K) (h₀ : A.comp M₀ = S)
    [Fintype (RowFiber A S)] (f : (E →ₗ[F2] K) → ℝ) :
    (𝔼 M : RowFiber A S, f M.val) =
      𝔼 N : E →ₗ[F2] A.ker, f (assemble A M₀ N) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.RowFiber, OAI.MaxCutGames.Decoder.AdviceFibers.assemble
abbrev OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow line 120
Source documentation
Only attainable rows are observation values.
```
abbrev ObservedRow (A : K →ₗ[F2] R) :=
…
```
def OAI.MaxCutGames.Decoder.AdviceFibers.observe line 123
def OAI.MaxCutGames.Decoder.AdviceFibers.observedBase line 127
Source documentation
A canonical base depends only on observed advice, never on the hidden matrix.
```
def observedBase (A : K →ₗ[F2] R) (S : ObservedRow (E := E) A) : E →ₗ[F2] K :=
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow
theorem OAI.MaxCutGames.Decoder.AdviceFibers.observedBase_property line 130
def OAI.MaxCutGames.Decoder.AdviceFibers.hiddenCoordinate line 133
theorem OAI.MaxCutGames.Decoder.AdviceFibers.observe_assemble_base line 138
def OAI.MaxCutGames.Decoder.AdviceFibers.observationEquiv line 145
Source documentation
Full matrix space is a product of attainable visible rows and private kernel-valued maps. A section of A is not required.
```
def observationEquiv (A : K →ₗ[F2] R) :
    (E →ₗ[F2] K) ≃ ObservedRow (E := E) A × (E →ₗ[F2] A.ker) where
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow
theorem OAI.MaxCutGames.Decoder.AdviceFibers.observationEquiv_apply line 165
theorem OAI.MaxCutGames.Decoder.AdviceFibers.observation_expect line 172
Source documentation
The joint law is exactly the uniform product law.
```
theorem observation_expect (f : ObservedRow (E := E) A → (E →ₗ[F2] A.ker) → ℝ) :
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow
theorem OAI.MaxCutGames.Decoder.AdviceFibers.observed_hidden_independent line 181
Source documentation
Exact factorization of every product of visible and private observables.
```
theorem observed_hidden_independent (f : ObservedRow (E := E) A → ℝ)
…
```
Mentions: OAI.MaxCutGames.Decoder.AdviceFibers.ObservedRow
abbrev OAI.MaxCutGames.Reduction.ActualOrbit.Ambient line 204
def OAI.MaxCutGames.Reduction.ActualOrbit.body line 206
def OAI.MaxCutGames.Reduction.ActualOrbit.offset line 209
def OAI.MaxCutGames.Reduction.ActualOrbit.Vertex line 212
Source documentation
Only realized bodies are vertices; no extra formal records are added.
```
def Vertex (can : Q → Ambient s d × T) := {o : Vector d × T // ∃ q, body can q = o}
```
Mentions: OAI.MaxCutGames.Reduction.ActualOrbit.Ambient, OAI.MaxCutGames.Reduction.ActualOrbit.body
def OAI.MaxCutGames.Reduction.ActualOrbit.vertex line 214
theorem OAI.MaxCutGames.Reduction.ActualOrbit.vertex_surjective line 217
instance OAI.MaxCutGames.Reduction.ActualOrbit.vertexFintype line 222
instance OAI.MaxCutGames.Reduction.ActualOrbit.vertexNonempty line 227
theorem OAI.MaxCutGames.Reduction.ActualOrbit.vertex_eq_iff line 230
abbrev OAI.MaxCutGames.Reduction.ActualOrbit.TwoSidedVertex line 238
Source documentation
false is the left copy and true is the right copy.
```
abbrev TwoSidedVertex (can : Q → Ambient s d × T) := Bool × Vertex can
```
Mentions: OAI.MaxCutGames.Reduction.ActualOrbit.Ambient, OAI.MaxCutGames.Reduction.ActualOrbit.Vertex
def OAI.MaxCutGames.Reduction.ActualOrbit.vertexEquiv line 240
def OAI.MaxCutGames.Reduction.ActualOrbit.explicitVertexEquiv line 246
Source documentation
Executable vertex numbering from an exhaustive list, preserving the same realizable-body subtype used in the semantic statements.
```
def explicitVertexEquiv [DecidableEq (Vector d × T)]
    (can : Q → Ambient s d × T) (queries : List Q) (full : ∀ q, q ∈ queries) :
    Vertex can ≃ Fin (Encoding.imageVertices queries (body can)).length :=
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualOrbit.Ambient, OAI.MaxCutGames.Reduction.ActualOrbit.Vertex, OAI.MaxCutGames.Reduction.Encoding.imageVertices, OAI.MaxCutGames.Reduction.ActualOrbit.body
def OAI.MaxCutGames.Reduction.ActualOrbit.unfold line 258
theorem OAI.MaxCutGames.Reduction.ActualOrbit.add_self_vector line 261
theorem OAI.MaxCutGames.Reduction.ActualOrbit.add_cancel_vector line 265
theorem OAI.MaxCutGames.Reduction.ActualOrbit.constraint_iff_unfolded line 269
Source documentation
The precise orientation used by the generated edge.
```
theorem constraint_iff_unfolded (can : Q → Ambient s d × T)
    (labelL labelR : Vertex can → Vector s) (q r : Q) :
    (labelL (vertex can q) + offset can q) + offset can r = labelR (vertex can r) ↔
      unfold can labelL q = unfold can labelR r := by
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualOrbit.Ambient, OAI.MaxCutGames.Reduction.ActualOrbit.Vertex, OAI.MaxCutGames.Reduction.ActualOrbit.vertex, OAI.MaxCutGames.Reduction.ActualOrbit.offset, OAI.MaxCutGames.Reduction.ActualOrbit.unfold
theorem OAI.MaxCutGames.Reduction.ActualOrbit.unfold_eq_of_canonical_eq line 282
Source documentation
A common full canonical record has one common unfolded value on each side.
```
theorem unfold_eq_of_canonical_eq (can : Q → Ambient s d × T)
    (label : Vertex can → Vector s) (q r : Q) (h : can q = can r) :
    unfold can label q = unfold can label r := by
…
```
Mentions: OAI.MaxCutGames.Reduction.ActualOrbit.Ambient, OAI.MaxCutGames.Reduction.ActualOrbit.Vertex, OAI.MaxCutGames.Reduction.ActualOrbit.unfold