BlockDescentLemmas.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Outgoing harmonic loss for the actual adaptive child map

Uniform sampling of the concrete pair (field line, binary orientation) has the uniform field-line marginal. The child rank is independent of orientation, so the proved quadratic kernel count gives the outgoing conditional loss for the common map produced by every parent lift.

abbrev OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual line 21
def OAI.UniqueGamesTheorem.Gadget.BlockDescent.traceSpace line 24
Source documentation
Coordinates of a binary character subspace under the trace pairing.
```
def traceSpace (S : Submodule (ZMod 2) (BinaryDual (F := F))) :
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual
def OAI.UniqueGamesTheorem.Gadget.BlockDescent.traceSpaceEquiv line 27
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.traceSpace_finrank line 33
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.traceSpaceEquiv_apply_val line 38
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.traceSpaceEquiv_symm_val line 43
def OAI.UniqueGamesTheorem.Gadget.BlockDescent.traceLift line 52
Source documentation
One binary-linear lift on the trace-coordinate domain, obtained from the single common parent map. It is fixed before the outgoing line/orientation.
```
def traceLift (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.childCharacter_comp_traceSpaceEquiv line 57
Source documentation
Equality of actual child maps after a change of logical coordinates.
```
theorem childCharacter_comp_traceSpaceEquiv
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.childCharacter_range_eq line 77
Source documentation
The child logical image is unchanged by the trace-coordinate domain isomorphism. This is equality of subspaces, not merely equality of ranks.
```
theorem childCharacter_range_eq
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.childCharacter_range_eq_dual_pullback line 88
Source documentation
Before the orientation is revealed, the un-oriented image is fixed; the fresh isomorphism acts only by dual pullback on this fixed image.
```
theorem childCharacter_range_eq_dual_pullback
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual
theorem OAI.UniqueGamesTheorem.Gadget.BlockDescent.childCharacter_rank_independent line 98
Source documentation
The rank is independent of the fresh orientation.
```
theorem childCharacter_rank_independent
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
Mentions: OAI.UniqueGamesTheorem.Gadget.BlockDescent.BinaryDual
def OAI.UniqueGamesTheorem.Gadget.FreshGenericity.rankSpaceEquiv line 123
Source documentation
A fixed coordinate equivalence transports the complete rank-indexed Grassmannian bijectively, so it preserves its uniform distribution.
```
def rankSpaceEquiv (e : V ≃ₗ[K] W) (r : ℕ) : RankSpace K V r ≃ RankSpace K W r :=
…
```
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.rankSpaceEquiv_apply line 128
def OAI.UniqueGamesTheorem.Gadget.FreshGenericity.bad line 152
Source documentation
Nongenericity includes the universal lift quantifier in IsGeneric. The field's simultaneous bound includes rank zero as well.
```
def bad (S : Submodule (ZMod 2) (BinaryDual (F := F))) : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.mean_bad_rankSpace line 155
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.mean_fresh_bad_at_line line 174
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.unoriented_rank_le line 197
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.fresh_bad_at_line_le line 208
Source documentation
The field error bound applies to the actual fresh descendant rank, even though that rank depends on the earlier lift and the selected line.
```
theorem fresh_bad_at_line_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.fresh_bad_le line 223
Source documentation
Fresh nongenericity bound over the actual full child index. The parent family and the common-parent map are arbitrary fixed inputs, so the result applies at every adaptive history without a future-lift independence premise.
```
theorem fresh_bad_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
theorem OAI.UniqueGamesTheorem.Gadget.FreshGenericity.descendant_bad_le line 240
Source documentation
The fresh bound for the deterministic descendant of an actual parent lift. The common-parent map is chosen from the whole lift before sampling the child index, exactly as required by the adaptive finite-history experiment.
```
theorem descendant_bad_le
    [DecidableEq (BlockOrientationIndex F)] [Nonempty (BlockOrientationIndex F)] :
    let J := orientedBlockLinear (F := F)
…
```
def OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.outgoingLoss line 275
theorem OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.outgoingLoss_eq_line_average line 282
Source documentation
Averaging all binary orientations reduces exactly to the actual line-law rank experiment, after transporting logical characters by the trace pairing.
```
theorem outgoingLoss_eq_line_average
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
theorem OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.generic_outgoing_loss_le line 303
Source documentation
The generic all-lifts bound applies to the actual common parent map.
```
theorem generic_outgoing_loss_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
theorem OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.arbitrary_outgoing_loss_le line 312
Source documentation
Nongeneric actual child maps satisfy the fallback harmonic charge.
```
theorem arbitrary_outgoing_loss_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
theorem OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.badRankCoefficient_mono line 320
theorem OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.outgoing_harmonic_loss_le line 329
Source documentation
Combined conditional law with a coefficient frozen at the initial rank. The bad predicate is exactly the nongeneric trace-coordinate domain.
```
theorem outgoing_harmonic_loss_le
    (S : Submodule (ZMod 2) (BinaryDual (F := F)))
…
```
theorem OAI.UniqueGamesTheorem.Gadget.OutgoingHarmonic.descendant_harmonic_loss_le line 349
Source documentation
Direct instantiation of DescentProbability.expected_terminal_loss's outgoing-step hypothesis for the concrete child domain of every actual lift.
```
theorem descendant_harmonic_loss_le
    [DecidableEq (BlockOrientationIndex F)] [Nonempty (BlockOrientationIndex F)] :
    let J : BlockOrientationIndex F → Vec F →ₗ[ZMod 2] Vec F × Vec F :=
…
```
def OAI.UniqueGamesTheorem.Gadget.BaseDetection.logicalCharacters line 378
Source documentation
Turn the fixed generic vector subspace into its actual logical characters.
```
def logicalCharacters (S : Submodule (ZMod 2) (Vec F)) :
    Submodule (ZMod 2) (BinaryDual (F := F)) :=
…
```
theorem OAI.UniqueGamesTheorem.Gadget.BaseDetection.traceSpace_logicalCharacters line 384
theorem OAI.UniqueGamesTheorem.Gadget.BaseDetection.logicalCharacters_finrank line 390
theorem OAI.UniqueGamesTheorem.Gadget.BaseDetection.theta_pos line 396
theorem OAI.UniqueGamesTheorem.Gadget.BaseDetection.full_lift_detection line 403
Source documentation
All probabilities concern the actual recursive noise choices. The field and generic top space satisfy separately proved finite-field properties; no probability estimate for the whole recursive gadget is an input.
```
theorem full_lift_detection :
    let J : BlockOrientationIndex F → Vec F →ₗ[ZMod 2] Vec F × Vec F :=
…
```