InitialOracle.lean`

110 declarations, 0 contain sorry, 0 declared as axioms

InitialOracle

Actual initial scores and anchors, count partitions and typicality, clipped metadata, common decoding, sharp hidden-count energy, tails, and budget caps.

def OAI.TraceReconstruction.initialMomentRatio line 22
def OAI.TraceReconstruction.initialSignedBudget line 25
theorem OAI.TraceReconstruction.initialSignedBudget_nonneg line 29
theorem OAI.TraceReconstruction.initial_signed_moment line 40
Source documentation
The signed score numerator in the actual conditional mark-list laws, with the entire finite cancellation energy and geometric tail retained.
```
theorem initial_signed_moment {u m l R : ℕ} (hu : 0 < u) (hm : 128 ≤ m)
    (hum : u ≤ m) (hR : 0 < R) (hl : l ≤ u*m) (off : Fin m)
    (hi : 1 ≤ off.val ∧ off.val+1 < m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.initial_conditional_clipped_exists line 68
Source documentation
Quantitative normalized common clipping of the level-zero conditional pair. This theorem has only the literal count/geometric inequalities of the initial construction, not a signed-density or oracle conclusion premise.
```
theorem initial_conditional_clipped_exists {u m l R : ℕ} (hu : 0 < u) (hm : 128 ≤ m)
    (hum : u ≤ m) (hR : 0 < R) (hl : l ≤ u*m) (off : Fin m)
    (hi : 1 ≤ off.val ∧ off.val+1 < m) (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.FiniteLaw.evenMomentSq_le_of_expect line 119
theorem OAI.TraceReconstruction.FiniteLaw.tv_sigma_eq line 126
def OAI.TraceReconstruction.ClippedOracle.weaken line 140
def OAI.TraceReconstruction.ClippedOracle.trivial line 151
def OAI.TraceReconstruction.ClippedOracle.sigma line 167
Source documentation
Reported metadata is retained, so the squared moment of a normalized score assembles without a mixing penalty. No conditioning of the original latent metadata distribution occurs.
```
def sigma {ι : Type*} [Fintype ι] {β : ι → Type*} [∀i,Fintype (β i)]
    (M : FiniteLaw ι) (P Q : ∀i,FiniteLaw (β i)) (e : ι → ℝ)
    (k : ℕ) (hk : 1≤k) (V : ℝ) (hV : 0≤V)
    (C : ∀i,ClippedOracle (P i) (Q i) k (e i) V) :
    ClippedOracle (M.sigma P) (M.sigma Q) k (M.expect e) V where
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ClippedOracle

theorem OAI.TraceReconstruction.ClippedOracle.assemble_good line 198

Source documentation

Replace bad conditional observations by a common law rather than making the original metadata law conditional on typicality. The exact cost is the true metadata failure mass plus the good conditional clipping cost.

theorem assemble_good {ι : Type*} [Fintype ι] {β : ι → Type*} [∀i,Fintype (β i)]
    (M : FiniteLaw ι) (P Q : ∀i,FiniteLaw (β i)) (Good : ι → Prop)
    (k : ℕ) (hk : 1≤k) (e V : ℝ) (he : 0≤e) (hV : 0≤V)
    (C : ∀i,Good i → Nonempty (ClippedOracle (P i) (Q i) k e V)) :
    Nonempty (ClippedOracle (M.sigma P) (M.sigma Q) k
      (e+M.expect (fun i => if Good i then 0 else 1)) V) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ClippedOracle

theorem OAI.TraceReconstruction.translated_fair_eval line 223
def OAI.TraceReconstruction.posteriorAnchorSeries line 235
Source documentation
The literal initial anchor after conditioning the paired side outputs.
```
def posteriorAnchorSeries {ι : Type*} [Fintype ι] (c : ℤ) (d : ι → Option Bool) : IntSeries :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries
theorem OAI.TraceReconstruction.posterior_anchor_average line 239
theorem OAI.TraceReconstruction.posteriorAnchorSeries_nonneg line 250
theorem OAI.TraceReconstruction.posteriorAnchorSeries_total line 254
theorem OAI.TraceReconstruction.posteriorAnchorSeries_support line 262
theorem OAI.TraceReconstruction.posteriorAnchorSeries_central line 279
def OAI.TraceReconstruction.PairedMechanisms.emissionOracle line 293
theorem OAI.TraceReconstruction.PairedMechanisms.emission_factorization line 299
Source documentation
Bayes factorization is valid for arbitrary conditional finite emissions, including the dependent-length initial primitive-mark list.
```
theorem emission_factorization (M : PairedMechanisms Side J) (K : (Fin J → Bool) → FiniteLaw α) :
    (fairOrientations J).mixture (fun b => (M.reportsGiven b).prod (K b))=M.emissionOracle K := by
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.PairedMechanisms.fairOrientations
theorem OAI.TraceReconstruction.conditionalMotifLaw_posterior line 316
def OAI.TraceReconstruction.countedMotifLaw line 344
Source documentation
Initial observations retain the central count with its original binomial law.
```
def countedMotifLaw {u m : ℕ} (off : Fin m)
    (hsafe : SafeTaggedTuple (periodSlot (u:=u) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
theorem OAI.TraceReconstruction.countedMotifLaw_posterior line 352

def OAI.TraceReconstruction.motifOffset line 383

Source documentation

The actual displaced primitive slot in a period.

def motifOffset {m : ℕ} (off : Fin m) (hi : 1 ≤ off.val ∧ off.val+1 < m)
    (s : ℕ) (X : ℤ) (τ : ℝ) (j : ℤ) : Fin m :=
…

theorem OAI.TraceReconstruction.signedPeriodDefects_periodSlot line 389
def OAI.TraceReconstruction.motifPeriodWord line 400
theorem OAI.TraceReconstruction.signed_primitive_word line 404
theorem OAI.TraceReconstruction.motifOffset_outside line 413
theorem OAI.TraceReconstruction.motifOffset_translate line 421
theorem OAI.TraceReconstruction.periodString_three line 427

theorem OAI.TraceReconstruction.motifPeriodWord_window line 437

Source documentation

Every randomized initial partition is a partition of the same literal period string, with no fit conditioning or change of channel.

theorem motifPeriodWord_window {m : ℕ} (off : Fin m) (hi : 1 ≤ off.val ∧ off.val+1 < m)
    (t K z s : ℕ) (a : ℤ) (τ : ℝ) (hleft : (t:ℤ) ≤ a) (hright : a+(2^s:ℕ) ≤ t+K) :
    motifPeriodWord off hi (t+K+z) s a τ =
      pureAtomRun (initialPeriod m off.val) t ++ motifPeriodWord off hi K s (a-t) τ ++
      pureAtomRun (initialPeriod m off.val) z := by
…

Mentions: OAI.TraceReconstruction.motifPeriodWord, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.initialPeriod

theorem OAI.TraceReconstruction.motifPeriodWord_length line 459
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_expect_pairs line 470
def OAI.TraceReconstruction.decodePairedEmission line 503
Source documentation
Three chronological streams, with side pairs independent across slots. This forgets flags but does not separate any marks inside the central list.
```
def decodePairedEmission {Side α : Type*} {J : ℕ}
    (side : Side → List Bool) (central : α → List Bool) (z : Reports Side J × α) : List Bool :=
…
```
Mentions: OAI.TraceReconstruction.Reports
theorem OAI.TraceReconstruction.PairedMechanisms.reportsGiven_paired_simulates line 511
def OAI.TraceReconstruction.initialPrefixPeriods line 564
Source documentation
Exact initial paired prefix and complementary suffix sizes.
```
def initialPrefixPeriods {J : ℕ} (k : ℕ) (b : Fin J → Bool) : ℕ :=
…
```
def OAI.TraceReconstruction.initialSuffixPeriods line 566
theorem OAI.TraceReconstruction.initialPrefixPeriods_eval line 569
theorem OAI.TraceReconstruction.initialPairPeriods_total line 573
theorem OAI.TraceReconstruction.initialPrefixPeriods_bounds line 581
theorem OAI.TraceReconstruction.initial_paired_oracle_simulates line 590
abbrev OAI.TraceReconstruction.InitialMetadata line 673
abbrev OAI.TraceReconstruction.InitialObservation line 674
def OAI.TraceReconstruction.initialMetadataLaw line 677
def OAI.TraceReconstruction.initialConditionalLaw line 682
def OAI.TraceReconstruction.initialSigmaLaw line 690
def OAI.TraceReconstruction.decodeInitialObservation line 697
theorem OAI.TraceReconstruction.initialSigmaLaw_expect line 701
theorem OAI.TraceReconstruction.initial_sigma_simulates line 721
def OAI.TraceReconstruction.initialCountAdmissible line 738
Source documentation
This is the literal count-typicality condition; it does not change the central count's original binomial law.
```
def initialCountAdmissible (N : ℕ) (q : ℝ) (l : Fin (N+1)) : Prop :=
…
```
def OAI.TraceReconstruction.initialMetadataGood line 742
theorem OAI.TraceReconstruction.initial_sigma_clipped_exists line 749
Source documentation
The genuine initial metadata oracle is clipped by conditioning each admissible fiber only. Every bad report/count keeps its original mass and is replaced by a common law, so all discarded mass is charged.
```
theorem initial_sigma_clipped_exists {Side : Type*} [Fintype Side] {J K m R : ℕ}
    (M : PairedMechanisms Side J) (hK : 0 < K) (hm : 128 ≤ m) (hKm : K ≤ m)
    (hR : 0 < R) (off : Fin m) (hi : 1 ≤ off.val ∧ off.val+1 < m)
    (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=K) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot
def OAI.TraceReconstruction.purePeriodCoefficient line 790
theorem OAI.TraceReconstruction.mixedMotifCoefficient_pure_rank_difference line 794
def OAI.TraceReconstruction.initialPureDegreeBound line 804
Source documentation
The pure comparison retains all low-degree cancellation, not just its total defect density.
```
def initialPureDegreeBound (u m r s : ℕ) (π : IntSeries) (θ : ℝ) (l : ℕ) : ℝ :=
…
```
Mentions: OAI.TraceReconstruction.IntSeries
theorem OAI.TraceReconstruction.initialPureDegreeBound_nonneg line 811
theorem OAI.TraceReconstruction.pureMotif_degree_zero line 827
theorem OAI.TraceReconstruction.pureMotif_degree_cancellation line 835
theorem OAI.TraceReconstruction.purePeriod_degree_geometric line 851
theorem OAI.TraceReconstruction.pureMotif_degree_geometric line 879
def OAI.TraceReconstruction.initialPureBudget line 898
theorem OAI.TraceReconstruction.pure_initial_full_energy line 902
def OAI.TraceReconstruction.purePeriodDensity line 940
theorem OAI.TraceReconstruction.purePeriodDensity_nonneg line 943
theorem OAI.TraceReconstruction.purePeriodDensity_total line 950
theorem OAI.TraceReconstruction.purePeriodLaw_withDensity line 956
theorem OAI.TraceReconstruction.purePeriod_centered_energy line 965
theorem OAI.TraceReconstruction.purePeriod_centered_moment line 986
theorem OAI.TraceReconstruction.initial_pure_moment line 1007
theorem OAI.TraceReconstruction.initial_pure_conditional_clipped_exists line 1031
theorem OAI.TraceReconstruction.ClippedOracle.tracePair line 1084
Source documentation
A common finite decoder transfers normalized clipping to actual complete traces. Neither interface is permitted to assume the main lower bound.
```
theorem ClippedOracle.tracePair {α : Type} [Fintype α] {P Q : FiniteLaw α}
    {q e V : ℝ} {x y : List Bool} {k : ℕ} (f : α → List Bool)
    (C : ClippedOracle P Q k e V) (hP : SimulatesTrace q P f x)
    (hQ : SimulatesTrace q Q f y) : Nonempty (OracleTracePair q x y k e V) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ClippedOracle, OAI.TraceReconstruction.SimulatesTrace, OAI.TraceReconstruction.OracleTracePair
def OAI.TraceReconstruction.initialPureConditionalLaw line 1105
def OAI.TraceReconstruction.initialPureSigmaLaw line 1111
theorem OAI.TraceReconstruction.initialPureSigmaLaw_expect line 1116
theorem OAI.TraceReconstruction.initial_pure_sigma_simulates line 1129
theorem OAI.TraceReconstruction.initial_pure_sigma_clipped_exists line 1174
def OAI.TraceReconstruction.hiddenSignedL2Bound line 1216
Source documentation
The half-mean hidden-count event yields the correct L², not supremum, exponent J^{-s-1/2} in the initial Prouhet cancellation.
```
def hiddenSignedL2Bound (J s : ℕ) (ω : ℝ) : ℝ :=
…
```
def OAI.TraceReconstruction.hiddenUnsignedL2Bound line 1220
theorem OAI.TraceReconstruction.hiddenSignedL2Bound_nonneg line 1223
theorem OAI.TraceReconstruction.hiddenUnsignedL2Bound_nonneg line 1226
theorem OAI.TraceReconstruction.hidden_quotient_bound line 1229
theorem OAI.TraceReconstruction.posteriorAnchorSeries_signed_L2 line 1238
theorem OAI.TraceReconstruction.posteriorAnchorSeries_unsigned_L2 line 1254
def OAI.TraceReconstruction.initialDifferenceCap line 1276
theorem OAI.TraceReconstruction.initial_theta_variance line 1279
theorem OAI.TraceReconstruction.initialDifferenceCap_bound line 1290
def OAI.TraceReconstruction.initialPrefactorCap line 1303
Source documentation
All q dependence of a fixed rank-difference estimate is exposed here. The powers of u and m are retained exactly, including both large-gap gains.
```
def initialPrefactorCap (u m r d : ℕ) (q : ℝ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.initialPrefactorCap_nonneg line 1308
theorem OAI.TraceReconstruction.initial_prefactor_bound line 1312
theorem OAI.TraceReconstruction.binomial_mean_inverse_le_sqrt line 1320
def OAI.TraceReconstruction.initialRankTailCap line 1332
theorem OAI.TraceReconstruction.initial_rank_tail_bound line 1336
theorem OAI.TraceReconstruction.initialCountAdmissible_of_near line 1367
Source documentation
The central binomial typical interval also guarantees the rank-kernel variance condition, rather than imposing it by conditioning.
```
theorem initialCountAdmissible_of_near {N : ℕ} {q : ℝ}
    (hq : q∈Set.Ioc 0 (1/2:ℝ)) (hscale : 8≤(N:ℝ)*q^2) (l : Fin (N+1))
    (hnear : |(l.val:ℝ)-(N:ℝ)*(1-q^2/2)|<(N:ℝ)*q^2/4) :
    initialCountAdmissible N q l := by
…
```
Mentions: OAI.TraceReconstruction.initialCountAdmissible
theorem OAI.TraceReconstruction.initial_count_bad_mass line 1399
Source documentation
An explicit unconditional tail for the actual count law. Its q⁴ exponent is more than enough under the source's q⁻¹=N^{o(1)} standing regime.
```
theorem initial_count_bad_mass {N : ℕ} {q : ℝ}
    (hq : q∈Set.Ioc 0 (1/2:ℝ)) (hscale : 8≤(N:ℝ)*q^2) :
    (boundedCountLaw (le_refl N) (1-primitiveErasure q)
      (primitiveRetention_mem ⟨hq.1,by linarith [hq.2]⟩)).expect
      (fun l => if initialCountAdmissible N q l then 0 else 1) ≤
    2*Real.exp (-(N:ℝ)*q^4/64) := by
…
```
Mentions: OAI.TraceReconstruction.boundedCountLaw, OAI.TraceReconstruction.primitiveErasure, OAI.TraceReconstruction.primitiveRetention_mem, OAI.TraceReconstruction.initialCountAdmissible

theorem OAI.TraceReconstruction.initial_metadata_bad_mass line 1425

Source documentation

The true bad metadata mass is charged without changing any conditional law or requiring an unproved concentration conclusion.

theorem initial_metadata_bad_mass {Side : Type*} [Fintype Side] {J N : ℕ}
    (M : PairedMechanisms Side J) {q ω : ℝ}
    (hq : q∈Set.Ioc 0 (1/2:ℝ)) (hscale : 8≤(N:ℝ)*q^2)
    (hw : ∀i,M.hiddenWeight i=ω) (hp : ω^2∈Set.Icc 0 1) :
    (initialMetadataLaw M N ⟨hq.1,by linarith [hq.2]⟩).expect
      (fun z => if initialMetadataGood q ω z then 0 else 1) ≤
    2*Real.exp (-(N:ℝ)*q^4/64)+Real.exp (-(J:ℝ)*ω^4/16) := by
…

Mentions: OAI.TraceReconstruction.PairedMechanisms, OAI.TraceReconstruction.initialMetadataLaw, OAI.TraceReconstruction.initialMetadataGood

def OAI.TraceReconstruction.initialSignedPatternCap line 1459
def OAI.TraceReconstruction.initialPurePatternCap line 1465
theorem OAI.TraceReconstruction.initial_signed_pattern_cap line 1471
theorem OAI.TraceReconstruction.initial_pure_pattern_cap line 1492
def OAI.TraceReconstruction.initialSignedDegreeCap line 1513
def OAI.TraceReconstruction.initialPureDegreeCap line 1519
theorem OAI.TraceReconstruction.initial_signed_degree_cap line 1525
theorem OAI.TraceReconstruction.initial_pure_degree_cap line 1543
def OAI.TraceReconstruction.initialSignedCap line 1563
Source documentation
Scalar budgets independent of every actual report and count. The finite signed-pattern restriction is retained to preserve its three-difference gain.
```
def initialSignedCap (J u m R s : ℕ) (q ω w : ℝ) : ℝ :=
…
```
def OAI.TraceReconstruction.initialPureCap line 1567
theorem OAI.TraceReconstruction.initial_signed_budget_cap line 1571
theorem OAI.TraceReconstruction.initial_pure_budget_cap line 1584
def OAI.TraceReconstruction.OracleTracePair.weaken line 1604
def OAI.TraceReconstruction.initialErrorCap line 1612
theorem OAI.TraceReconstruction.actual_initial_oracles line 1619
Source documentation
Both required initial comparisons are genuine approximate complete-trace oracles. The metadata budgets have been eliminated: only explicit finite scalar bounds and literal period geometry remain to be instantiated.
```
theorem actual_initial_oracles {J K m R : ℕ}
    (hK : 0 < K) (hm : 128 ≤ m) (hKm : K ≤ m) (hR : 0 < R)
    (off : Fin m) (hi : 1 ≤ off.val ∧ off.val+1 < m)
    (hoff : |(off.val:ℝ)-(m:ℝ)/2| ≤ 2)
    (hsafe : SafeTaggedTuple (periodSlot (u:=K) (fun _ => off)))
…
```
Mentions: OAI.TraceReconstruction.SafeTaggedTuple, OAI.TraceReconstruction.periodSlot