Model.lean`

82 declarations, 0 contain sorry, 0 declared as axioms

Model

Independent deletion, complete trace observations, randomized estimators, ENNReal fixed-budget complexity, concatenation, and literal input words.

abbrev OAI.TraceReconstruction.Word line 19
Also declared: ComparatorChallenges/TraceReconstruction.lean:10 (same declaration text).
abbrev OAI.TraceReconstruction.Mask line 20
Also declared: ComparatorChallenges/TraceReconstruction.lean:11 (same declaration text).
abbrev OAI.TraceReconstruction.Trace line 21
Also declared: ComparatorChallenges/TraceReconstruction.lean:12 (same declaration text).
def OAI.TraceReconstruction.traceOfMask line 24
Source documentation
true retains the bit. The observer gets only the resulting list.
Also declared: ComparatorChallenges/TraceReconstruction.lean:15 (same declaration text).
```
def traceOfMask {n : ℕ} (x : Word n) (a : Mask n) : Trace :=
…
```
Mentions: OAI.TraceReconstruction.Word, OAI.TraceReconstruction.Mask, OAI.TraceReconstruction.Trace
def OAI.TraceReconstruction.maskWeight line 28
Source documentation
The deletion-mask probability, with deletion probability q.
Also declared: ComparatorChallenges/TraceReconstruction.lean:19 (same declaration text).
```
def maskWeight {n : ℕ} (q : ℝ) (a : Mask n) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.Mask
def OAI.TraceReconstruction.traceMass line 32
Source documentation
Law of a single complete trace.
Also declared: ComparatorChallenges/TraceReconstruction.lean:23 (same declaration text).
```
def traceMass {n : ℕ} (q : ℝ) (x : Word n) (w : Trace) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.Word, OAI.TraceReconstruction.Trace
def OAI.TraceReconstruction.traceSpace line 36
Source documentation
All possible complete outputs from length-n inputs, with lengths included.
Also declared: ComparatorChallenges/TraceReconstruction.lean:27 (same declaration text).
```
def traceSpace (n : ℕ) : Finset Trace :=
…
```
Mentions: OAI.TraceReconstruction.Trace
def OAI.TraceReconstruction.traceTV line 41
Source documentation
1/2 sum of absolute differences, on the full finite output space.
Also declared: ComparatorChallenges/TraceReconstruction.lean:32 (same declaration text).
```
def traceTV {n : ℕ} (q : ℝ) (x y : Word n) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.Word
def OAI.TraceReconstruction.IsEstimator line 46
Source documentation
The estimator may depend arbitrarily on n, q and every complete sample. Its value is its conditional probability of reporting the given input.
Also declared: ComparatorChallenges/TraceReconstruction.lean:37 (same declaration text).
```
def IsEstimator {n m : ℕ} (A : (Fin m → Trace) → Word n → ℝ) : Prop :=
…
```
Mentions: OAI.TraceReconstruction.Trace, OAI.TraceReconstruction.Word
def OAI.TraceReconstruction.reconstructionSuccess line 51
Source documentation
Independent masks generate independent complete traces; no retained positions, boundaries or other latent variables are revealed to A.
Also declared: ComparatorChallenges/TraceReconstruction.lean:42 (same declaration text).
```
def reconstructionSuccess {n m : ℕ} (q : ℝ)
    (A : (Fin m → Trace) → Word n → ℝ) (x : Word n) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.Trace, OAI.TraceReconstruction.Word
def OAI.TraceReconstruction.SufficientBudget line 56
Also declared: ComparatorChallenges/TraceReconstruction.lean:47 (same declaration text).
def OAI.TraceReconstruction.sampleComplexity line 61
Source documentation
Natural fixed sample budget; infimum of the empty set is infinity.
Also declared: ComparatorChallenges/TraceReconstruction.lean:52 (same declaration text).
```
noncomputable def sampleComplexity (n : ℕ) (q s : ℝ) : ℝ≥0∞ :=
…
```
def OAI.TraceReconstruction.minTraceTV line 65
Source documentation
The real infimum is a minimum for n>0 (a nonempty finite set).
Distinct definitions of this name: ComparatorChallenges/TraceReconstruction.lean:56 (same statement text; different proof or body). Qualify references as OAI.TraceReconstruction.minTraceTV@path.
```
noncomputable def minTraceTV (n : ℕ) (q : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.traceOfMask_length_le line 79
theorem OAI.TraceReconstruction.mem_traceSpace_of_length_le line 83
theorem OAI.TraceReconstruction.length_le_of_mem_traceSpace line 89
theorem OAI.TraceReconstruction.mem_traceSpace line 95
theorem OAI.TraceReconstruction.traceOfMask_mem line 99
theorem OAI.TraceReconstruction.maskWeight_nonneg line 103
theorem OAI.TraceReconstruction.sum_maskWeight line 109
theorem OAI.TraceReconstruction.traceMass_nonneg line 117
theorem OAI.TraceReconstruction.traceMass_eq_zero_of_not_mem line 125
theorem OAI.TraceReconstruction.sum_traceMass line 134
theorem OAI.TraceReconstruction.traceTV_nonneg line 140
theorem OAI.TraceReconstruction.traceTV_self line 144
theorem OAI.TraceReconstruction.traceTV_comm line 147
theorem OAI.TraceReconstruction.traceTV_le_one line 150
theorem OAI.TraceReconstruction.FiniteLaw.ext line 169
def OAI.TraceReconstruction.FiniteLaw.pure line 174
def OAI.TraceReconstruction.FiniteLaw.map line 179
theorem OAI.TraceReconstruction.FiniteLaw.map_mass line 182
theorem OAI.TraceReconstruction.FiniteLaw.expectation_map line 191
theorem OAI.TraceReconstruction.FiniteLaw.tv_map_le line 200
abbrev OAI.TraceReconstruction.BoundedTrace line 205
def OAI.TraceReconstruction.maskLaw line 207
def OAI.TraceReconstruction.completeTraceLaw line 210
theorem OAI.TraceReconstruction.completeTraceLaw_tv line 216
theorem OAI.TraceReconstruction.completeTraceLaw_mask line 222
theorem OAI.TraceReconstruction.trace_expectation line 235
def OAI.TraceReconstruction.appendWord line 247
Source documentation
Concatenation of exact binary inputs, not an encoded surrogate.
```
def appendWord {n m : ℕ} (x : Word n) (y : Word m) : Word (n + m) := Fin.append x y
```
Mentions: OAI.TraceReconstruction.Word
theorem OAI.TraceReconstruction.trace_filterMap line 249
theorem OAI.TraceReconstruction.traceOfMask_append line 265
theorem OAI.TraceReconstruction.maskWeight_append line 274
theorem OAI.TraceReconstruction.concatenated_trace_expectation line 280
abbrev OAI.TraceReconstruction.PrimitiveMark line 299
Source documentation
The four complete traces possible from the ordinary primitive 01.
```
abbrev PrimitiveMark := Fin 4
```
def OAI.TraceReconstruction.primitiveOutput line 301
def OAI.TraceReconstruction.ordinaryPrimitiveMass line 302
def OAI.TraceReconstruction.defectPrimitiveMass line 304
def OAI.TraceReconstruction.primitiveErasure line 305
def OAI.TraceReconstruction.primitiveMarkMass line 307
theorem OAI.TraceReconstruction.primitive_retain_pos line 311
theorem OAI.TraceReconstruction.primitiveMarkMass_nonneg line 316
theorem OAI.TraceReconstruction.primitiveMarkMass_sum line 323
def OAI.TraceReconstruction.primitiveMarkLaw line 332
theorem OAI.TraceReconstruction.primitiveMark_simulation line 338
Source documentation
Emitting the conditional mark, or silently erasing the block, gives exactly the ordinary primitive-output probabilities. Silent erasure and an emitted empty mark are distinct latent events.
```
theorem primitiveMark_simulation {q : ℝ} (hq : q ∈ Set.Ioo 0 1)
    (b : Bool) (z : PrimitiveMark) :
    (if z = 0 then primitiveErasure q else 0) +
      (1 - primitiveErasure q) * primitiveMarkMass q b z =
        if b then defectPrimitiveMass q z else ordinaryPrimitiveMass q z := by
…
```
Mentions: OAI.TraceReconstruction.PrimitiveMark, OAI.TraceReconstruction.primitiveErasure, OAI.TraceReconstruction.primitiveMarkMass, OAI.TraceReconstruction.defectPrimitiveMass, OAI.TraceReconstruction.ordinaryPrimitiveMass
def OAI.TraceReconstruction.primitiveScore line 347
theorem OAI.TraceReconstruction.primitive_score_identity line 349
theorem OAI.TraceReconstruction.primitive_score_centered line 358
theorem OAI.TraceReconstruction.primitive_score_bound line 365
theorem OAI.TraceReconstruction.primitive_score_variance_exact line 372
theorem OAI.TraceReconstruction.primitive_score_variance_le line 383
def OAI.TraceReconstruction.ordinaryRun line 399
theorem OAI.TraceReconstruction.ordinaryRun_length line 403
theorem OAI.TraceReconstruction.ordinaryRun_add line 408
def OAI.TraceReconstruction.initialPeriod line 414
Source documentation
A period of m primitives with its unique 1 defect at zero-based slot d.
```
def initialPeriod (m d : ℕ) : List Bool :=
…
```
theorem OAI.TraceReconstruction.initialPeriod_length line 417
theorem OAI.TraceReconstruction.initialPeriod_tail_ne line 423
Source documentation
Distinct defect slots differ before either period ends, independently of future text.
```
theorem initialPeriod_tail_ne {m d e : ℕ} (hde : d < e) (he : e < m)
    (u v : List Bool) : initialPeriod m d ++ u ≠ initialPeriod m e ++ v := by
…
```
Mentions: OAI.TraceReconstruction.initialPeriod
theorem OAI.TraceReconstruction.initialPeriod_injective line 437
def OAI.TraceReconstruction.periodString line 446
theorem OAI.TraceReconstruction.periodString_cons line 449
theorem OAI.TraceReconstruction.periodString_length line 454
theorem OAI.TraceReconstruction.periodString_injective line 462
def OAI.TraceReconstruction.atomString line 482
Source documentation
Uniformly sized binary atoms concatenated without boundary marks.
```
def atomString (P : ℕ) (w : Bool → List Bool) (θ : Fin P → Bool) : List Bool :=
…
```
theorem OAI.TraceReconstruction.atomString_cons line 485
theorem OAI.TraceReconstruction.atomString_length line 489
theorem OAI.TraceReconstruction.atomString_injective line 495
def OAI.TraceReconstruction.templateType line 515
Source documentation
Zero-based notation for the source complementary template; true is minus. The motif itself is fixed independently of the hypothesis.
```
def templateType (P a L : ℕ) (sign : Fin L → Bool) (τ : Bool) (i : Fin P) : Bool :=
…
```
theorem OAI.TraceReconstruction.templateType_at line 518
theorem OAI.TraceReconstruction.templateType_injective line 523
def OAI.TraceReconstruction.complementaryWords line 531
theorem OAI.TraceReconstruction.complementaryWords_length line 534
theorem OAI.TraceReconstruction.complementaryWords_injective line 538