RepresentationSurvival.lean`

86 declarations, 0 contain sorry, 0 declared as axioms

The representation experiment preceding the extra prime

The sample space retains each draw in order. The subblock partitions and the residue spaces use conditional uniform laws on their actual domains. Representative selection is a deterministic analysis function of this history; it does not inspect the extra prime or the separating families.

structure OAI.LowSpaceSubsetSum.RepresentationSetup line 26
Source documentation
A fixed YES instance and the three pre-order mixer locations.
```
structure RepresentationSetup (n : ℕ) where
…
```
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.Layout line 38
def OAI.LowSpaceSubsetSum.RepresentationSetup.originalWeights line 40
def OAI.LowSpaceSubsetSum.RepresentationSetup.signMask line 42
def OAI.LowSpaceSubsetSum.RepresentationSetup.signedWeights line 44
def OAI.LowSpaceSubsetSum.RepresentationSetup.signedTarget line 46
def OAI.LowSpaceSubsetSum.RepresentationSetup.signCoordinates line 49
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.signCoordinates_uniform line 55
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.signed_solution line 60
def OAI.LowSpaceSubsetSum.RepresentationSetup.rawMixers line 69
def OAI.LowSpaceSubsetSum.RepresentationSetup.mixerOrder line 72
def OAI.LowSpaceSubsetSum.RepresentationSetup.orderedMixers line 75
def OAI.LowSpaceSubsetSum.RepresentationSetup.selectedHalves line 78
def OAI.LowSpaceSubsetSum.RepresentationSetup.halfSize line 81
def OAI.LowSpaceSubsetSum.RepresentationSetup.lowExponent line 83
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodLayout line 87
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.halfSize_eq line 91
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.orderedMixers_card line 95
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.selectedHalves_subset line 101
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.selectedHalves_card line 104
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.selectedHalves_deficiency line 109
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.lowExponent_nonneg line 116
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.lowExponent_le_halfSize line 125
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.lowExponent_antitone line 132
def OAI.LowSpaceSubsetSum.RepresentationSetup.factorExponents line 143
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.prefixExponent_eq_floor line 148
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.factorExponents_le_scale line 162
def OAI.LowSpaceSubsetSum.RepresentationSetup.SizeGood line 183
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenSize line 188
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenSize_spec line 191
def OAI.LowSpaceSubsetSum.RepresentationSetup.guessRange line 238
Source documentation
The precise interval sampled by the implementation.
```
def guessRange (n : ℕ) : Finset ℕ :=
…
```
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses line 241
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guessRange_nonempty line 243
instance OAI.LowSpaceSubsetSum.RepresentationSetup.guessesNonempty line 248
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodGuesses line 251
def OAI.LowSpaceSubsetSum.RepresentationSetup.blockCount line 254
def OAI.LowSpaceSubsetSum.RepresentationSetup.blockHalf line 256
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.blockCount_half line 259
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.Partition line 269
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.Partitions line 273
instance OAI.LowSpaceSubsetSum.RepresentationSetup.partitionNonempty line 275
instance OAI.LowSpaceSubsetSum.RepresentationSetup.partitionsNonempty line 284
def OAI.LowSpaceSubsetSum.RepresentationSetup.Prescribed line 287
def OAI.LowSpaceSubsetSum.RepresentationSetup.retainedWeights line 295
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodPartitions line 301
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.PrimeSpace line 305
instance OAI.LowSpaceSubsetSum.RepresentationSetup.primeSpaceNonempty line 308
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.Residues line 311
instance OAI.LowSpaceSubsetSum.RepresentationSetup.residuesNonempty line 314
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodPrime line 318
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.GuessHistory line 323
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.PartitionHistory line 324
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.PrimeHistory line 325
abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.TrialHistory line 326
def OAI.LowSpaceSubsetSum.RepresentationSetup.layoutLaw line 328
def OAI.LowSpaceSubsetSum.RepresentationSetup.guessLaw line 330
def OAI.LowSpaceSubsetSum.RepresentationSetup.partitionLaw line 333
def OAI.LowSpaceSubsetSum.RepresentationSetup.primeLaw line 336
def OAI.LowSpaceSubsetSum.RepresentationSetup.trialLaw line 339
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.mixerSize_add_one_le_scale line 342
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.goodLayout_probability line 351
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.goodGuesses_probability line 383
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.goodPartitions_probability line 427
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.retainedWeight_bound line 473
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.goodPrime_probability line 479
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodGuessHistory line 497
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodPartitionHistory line 500
def OAI.LowSpaceSubsetSum.RepresentationSetup.GoodPrimeHistory line 503
structure OAI.LowSpaceSubsetSum.RepresentationSetup.ResidueOffsets line 508
Source documentation
The offsets may depend on the layout, guesses, and subblock partition; they are fixed before the common prime tuple and its target residues.
```
structure ResidueOffsets where
…
```
def OAI.LowSpaceSubsetSum.RepresentationSetup.ResidueSuccess line 513
def OAI.LowSpaceSubsetSum.RepresentationSetup.Successful line 521
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.residueSuccess_probability line 524

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.successful_probability line 541

Source documentation

All probability factors are proved for the concrete successive draws. No success probability is assumed as an interface.

theorem successful_probability (O : R.ResidueOffsets)
    (hn : 180000000 ≤ n)
    (hmean : meanDeficiency R.originalWeights Finset.univ R.halfSize <
      (153 / 20000 : ℝ) * n)
    (hden : (R.halfSize : ℝ) + 1 <
      (2 : ℝ) ^ ((1 / 1500 : ℝ) * R.halfSize)) :
    1 / (inputScale R.input : ℝ) ^ 100 ≤ R.trialLaw.probability (R.Successful O) := by
…

Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.mem_retainedWeights line 600
def OAI.LowSpaceSubsetSum.RepresentationSetup.retainedMask line 610
Source documentation
The lookup is a deterministic analysis choice on distinct retained weights.
```
def retainedMask (z : Layout n) (g : Guesses n) (f : R.Partitions z)
    (i : Fin 3) (x : ℤ) : Finset (Fin n) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.retainedMask_spec line 617
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenWeights line 634
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenMasks line 642

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenTop_independent_children line 647

Source documentation

In particular, the top choice is fixed before either child residue.

theorem chosenTop_independent_children (O : R.ResidueOffsets) (h : R.PrimeHistory)
    (r s : R.Residues h.2) (hrs : r.1 = s.1) :
    R.chosenMasks O h r 0 = R.chosenMasks O h s 0 := by
…

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenWeights_mem line 652
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenMasks_spec line 663
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.successful_spread line 674
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenWeights_compatible line 683

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.future_conditional_product line 712

Source documentation

Later randomness may depend on the retained layout, but not on an analysis witness. Its conditional joint law remains the prescribed product.

theorem future_conditional_product
    (Q F : R.TrialHistory → Type*) [∀ h, Fintype (Q h)] [∀ h, Fintype (F h)]
    [∀ h, Nonempty (Q h)] [∀ h, Nonempty (F h)]
    (A : ∀ h, Q h → Prop) (B : ∀ h, F h → Prop)
    (h : R.TrialHistory) (hh : R.trialLaw.mass h ≠ 0) :
    (R.trialLaw.bind (fun x => Q x × F x) (fun _ => FiniteLaw.uniform)).probability
        (fun z => z.1 = h ∧ A z.1 z.2.1 ∧ B z.1 z.2.2) /
      R.trialLaw.probability (fun x => x = h) =
      finiteUniformProbability (A h) * finiteUniformProbability (B h) := by
…

Mentions: OAI.LowSpaceSubsetSum.FiniteLaw.uniform, OAI.LowSpaceSubsetSum.finiteUniformProbability

theorem OAI.LowSpaceSubsetSum.eventually_representation_half_gap line 729
theorem OAI.LowSpaceSubsetSum.eventually_representation_survival line 748
Source documentation
A uniform threshold works for every input and every fixed solution; the logarithmic representative loss is discharged rather than assumed.
```
theorem eventually_representation_survival :
    ∃ N : ℕ, ∀ n ≥ N, ∀ R : RepresentationSetup n,
      meanDeficiency R.originalWeights Finset.univ R.halfSize <
        (153 / 20000 : ℝ) * n →
      ∀ O : R.ResidueOffsets,
        1 / (inputScale R.input : ℝ) ^ 100 ≤ R.trialLaw.probability (R.Successful O) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup, OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.inputScale