Oracles.lean`

141 declarations, 0 contain sorry, 0 declared as axioms

Oracles

TV kernels and trace simulation, anchor costs, counted primitives, common-part lifting, concrete oracle pairs, and paired-flag metadata.

theorem OAI.TraceReconstruction.FiniteLaw.law_ext line 23
theorem OAI.TraceReconstruction.FiniteLaw.tv_self line 26
theorem OAI.TraceReconstruction.FiniteLaw.tv_le_one line 28
theorem OAI.TraceReconstruction.FiniteLaw.expect_bind line 37
theorem OAI.TraceReconstruction.FiniteLaw.bind_assoc line 48
theorem OAI.TraceReconstruction.FiniteLaw.tv_bind_kernel_le line 60

theorem OAI.TraceReconstruction.FiniteLaw.tv_bind_fit_le line 88

Source documentation

An invalid layout is charged only its unconditional probability.

theorem tv_bind_fit_le (P : FiniteLaw α) (K L : α → FiniteLaw β)
    (good : α → Prop) [DecidablePred good] (E : ℝ)
    (hfit : ∀a,good a → (K a).tv (L a)≤E) :
    (P.bind K).tv (P.bind L) ≤ P.expect (fun a => if good a then E else 1) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.tv

theorem OAI.TraceReconstruction.FiniteLaw.tv_prod_eq_left line 99
theorem OAI.TraceReconstruction.FiniteLaw.tv_prod_eq_right line 108
theorem OAI.TraceReconstruction.FiniteLaw.tv_prod_le line 116
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_succ_tv line 129
theorem OAI.TraceReconstruction.FiniteLaw.tv_coordinateProduct_le line 141
theorem OAI.TraceReconstruction.FiniteLaw.expect_coordinateProduct_succ line 149
theorem OAI.TraceReconstruction.FiniteLaw.expect_sub line 167
theorem OAI.TraceReconstruction.FiniteLaw.abs_expect_le line 171
def OAI.TraceReconstruction.SimulatesTrace line 179
Source documentation
A finite auxiliary observation, decoded by a fixed function, simulates the usual deletion channel on a literal binary word. Test functions range over the observable traces only, never latent boundaries.
```
def SimulatesTrace {α : Type*} [Fintype α] (q : ℝ) (P : FiniteLaw α)
    (decode : α → List Bool) (w : List Bool) : Prop :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
def OAI.TraceReconstruction.ApproximatesTrace line 183
theorem OAI.TraceReconstruction.listDeletionExpectation_const line 188
theorem OAI.TraceReconstruction.listDeletionExpectation_linear line 194
theorem OAI.TraceReconstruction.listDeletionExpectation_mono line 202
theorem OAI.TraceReconstruction.listDeletionExpectation_range line 211
theorem OAI.TraceReconstruction.listDeletionExpectation_sum line 220
theorem OAI.TraceReconstruction.FiniteLaw.expect_listDeletionExpectation line 229
theorem OAI.TraceReconstruction.SimulatesTrace.append line 240
theorem OAI.TraceReconstruction.SimulatesTrace.approximate line 253
theorem OAI.TraceReconstruction.ApproximatesTrace.append line 259
theorem OAI.TraceReconstruction.SimulatesTrace.random_partition line 279
Source documentation
Any randomized partition into exactly the same literal word gives exactly its usual trace after boundaries are forgotten. No fit conditioning occurs.
```
theorem SimulatesTrace.random_partition {α Ω : Type*} [Fintype α] [Fintype Ω]
    {q : ℝ} (P : FiniteLaw Ω) (K : Ω → FiniteLaw α) (decode : α → List Bool)
    (w : List Bool) (h : ∀ω,SimulatesTrace q (K ω) decode w) :
    SimulatesTrace q (P.bind K) decode w := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.SimulatesTrace

theorem OAI.TraceReconstruction.ApproximatesTrace.random_partition line 291

Source documentation

A failed deterministic layout is charged its unconditional probability; the conditional law on all metadata, not a fit-conditioned law, is used.

theorem ApproximatesTrace.random_partition {α Ω : Type*} [Fintype α] [Fintype Ω]
    {q : ℝ} (hq : q∈Set.Icc 0 1) (P : FiniteLaw Ω) (K : Ω → FiniteLaw α)
    (decode : α → List Bool) (w : List Bool) (good : Ω → Prop) [DecidablePred good]
    (E : ℝ) (h : ∀ω,good ω → ApproximatesTrace q (K ω) decode w E) :
    ApproximatesTrace q (P.bind K) decode w (P.expect (fun ω => if good ω then E else 1)) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ApproximatesTrace

def OAI.TraceReconstruction.closeLabels line 318
Source documentation
Admissible close child labels, without relaxing any plateau restrictions on the anchor. An arbitrary finite label domain is retained.
```
def closeLabels (A : Finset ℤ) (L : ℕ) (a : ℤ) : Finset ℤ :=
…
```
theorem OAI.TraceReconstruction.closeLabels_card line 321
theorem OAI.TraceReconstruction.root_anchor_energy line 333
Source documentation
Root anchor and close-child energy. This keeps the actual labels finite, including any additional source plateau cutoff.
```
theorem root_anchor_energy (n L : ℕ) (A B : Finset ℤ) (c : ℤ) :
    (∑ a∈A, ∑ _d∈closeLabels B L a, windowKernel n L (a-c)^2) ≤
      2*L^3*binomialBound n := by
…
```
Mentions: OAI.TraceReconstruction.closeLabels, OAI.TraceReconstruction.windowKernel, OAI.TraceReconstruction.binomialBound
theorem OAI.TraceReconstruction.sibling_anchor_energy line 349
Source documentation
The shared global jitter stays in the joint kernel until after squaring. The two close labels cost only (2L)^2, uniformly in parent labels.
```
theorem sibling_anchor_energy (g n₁ n₂ L : ℕ) (A B C D : Finset ℤ) (c₁ c₂ : ℤ) :
    (∑ a∈A, ∑ b∈B, ∑ _c∈closeLabels C L a, ∑ _d∈closeLabels D L b,
      jointWindowKernel g n₁ n₂ L (a-c₁) (b-c₂)^2) ≤
      4*L^6*binomialBound g*binomialBound n₂ := by
…
```
Mentions: OAI.TraceReconstruction.closeLabels, OAI.TraceReconstruction.jointWindowKernel, OAI.TraceReconstruction.binomialBound
def OAI.TraceReconstruction.binaryTreeSum line 373
Source documentation
Exact bottom-up summation of any finite binary anchor model. The state contains its actual index path, so group-dependent kernels are allowed.
```
def binaryTreeSum {α : Type*} [Fintype α] (K : ℕ → α → α × α → ℝ) : ℕ → α → ℝ
  | 0, _ => 1
  | n+1, a => ∑b, K n a b*binaryTreeSum K n b.1*binaryTreeSum K n b.2
```
def OAI.TraceReconstruction.binaryTreeBudget line 377
theorem OAI.TraceReconstruction.binaryTreeBudget_nonneg line 381
theorem OAI.TraceReconstruction.binaryTreeSum_nonneg line 387
theorem OAI.TraceReconstruction.binaryTreeSum_le line 397
Source documentation
Uniform local anchor square sums multiply without decoupling the two correlated offsets of a sibling group. Domain/plateau indicators can be included in K and are never removed by conditioning.
```
theorem binaryTreeSum_le {α : Type*} [Fintype α]
    (K : ℕ → α → α × α → ℝ) (hK : ∀n a b,0≤K n a b)
    (C : ℕ → ℝ) (hC : ∀n,0≤C n) (hlocal : ∀n a, (∑b,K n a b)≤C n)
    (n : ℕ) (a : α) : binaryTreeSum K n a≤binaryTreeBudget C n := by
…
```
Mentions: OAI.TraceReconstruction.binaryTreeSum, OAI.TraceReconstruction.binaryTreeBudget
theorem OAI.TraceReconstruction.hypergeomMass_middle_sq line 420
theorem OAI.TraceReconstruction.hypergeomMass_middle_le line 442
theorem OAI.TraceReconstruction.sum_range_extend_zero line 453
theorem OAI.TraceReconstruction.hypergeomMass_above_total line 460
def OAI.TraceReconstruction.hypergeomLaw line 463
theorem OAI.TraceReconstruction.hypergeomMass_complement line 472
theorem OAI.TraceReconstruction.hypergeomLaw_adjacent_tv line 477
theorem OAI.TraceReconstruction.adjacentHypergeomTV_middle_le line 512
theorem OAI.TraceReconstruction.hypergeomLaw_adjacent_middle line 521
theorem OAI.TraceReconstruction.FiniteLaw.tv_chain line 537
theorem OAI.TraceReconstruction.hypergeomLaw_steps line 545
def OAI.TraceReconstruction.visibleFiberEquiv line 573
def OAI.TraceReconstruction.visibleScheduleLaw line 585
theorem OAI.TraceReconstruction.visibleScheduleLaw_mass line 588
theorem OAI.TraceReconstruction.sum_finset_card line 614
theorem OAI.TraceReconstruction.visibleScheduleLaw_tv line 643
theorem OAI.TraceReconstruction.visibleScheduleLaw_steps line 678
theorem OAI.TraceReconstruction.FiniteLaw.ext_expect line 695
theorem OAI.TraceReconstruction.FiniteLaw.expect_map line 701
theorem OAI.TraceReconstruction.FiniteLaw.map_map line 704
theorem OAI.TraceReconstruction.FiniteLaw.map_id line 711
theorem OAI.TraceReconstruction.FiniteLaw.map_equiv_mass line 717
theorem OAI.TraceReconstruction.FiniteLaw.tv_map_equiv line 722
def OAI.TraceReconstruction.fixedSubsetEquiv line 732
theorem OAI.TraceReconstruction.uniformSubsetLaw_map line 738
abbrev OAI.TraceReconstruction.HiddenIndex line 752
abbrev OAI.TraceReconstruction.VisibleIndex line 753
def OAI.TraceReconstruction.splitIndexEquiv line 755
theorem OAI.TraceReconstruction.card_splitIndex line 758
theorem OAI.TraceReconstruction.card_hiddenIndex line 763
def OAI.TraceReconstruction.eraseScheduleLaw line 766
theorem OAI.TraceReconstruction.erase_splitIndex line 770
theorem OAI.TraceReconstruction.eraseScheduleLaw_eq line 796
theorem OAI.TraceReconstruction.eraseScheduleLaw_steps line 809
def OAI.TraceReconstruction.FiniteLaw.sigma line 833
theorem OAI.TraceReconstruction.FiniteLaw.expect_sigma line 841
theorem OAI.TraceReconstruction.FiniteLaw.overlap_sigma_lower line 845
theorem OAI.TraceReconstruction.sum_binomialMass_cutoff line 857
def OAI.TraceReconstruction.boundedCountLaw line 867
abbrev OAI.TraceReconstruction.BoundedMarks line 872
def OAI.TraceReconstruction.boundedConditionalPrimitiveLaw line 874
theorem OAI.TraceReconstruction.primitiveRetention_mem line 878
def OAI.TraceReconstruction.countedPrimitiveLaw line 884
def OAI.TraceReconstruction.decodeBoundedMarks line 889
theorem OAI.TraceReconstruction.countedPrimitiveLaw_expect line 891
theorem OAI.TraceReconstruction.countedPrimitiveLaw_simulates line 919
theorem OAI.TraceReconstruction.subsetLaw_expect_card line 935
theorem OAI.TraceReconstruction.subsetLaw_variance line 946
def OAI.TraceReconstruction.hiddenScheduleLaw line 952
theorem OAI.TraceReconstruction.hiddenScheduleLaw_tv line 956
theorem OAI.TraceReconstruction.good_hiddenSchedule_bound line 967
theorem OAI.TraceReconstruction.bad_hiddenSchedule_variance line 985
theorem OAI.TraceReconstruction.hiddenScheduleLaw_steps line 996
theorem OAI.TraceReconstruction.FiniteLaw.expect_comm line 1046
theorem OAI.TraceReconstruction.FiniteLaw.bind_map line 1056
theorem OAI.TraceReconstruction.FiniteLaw.map_bind line 1063
theorem OAI.TraceReconstruction.FiniteLaw.bind_comm line 1069
theorem OAI.TraceReconstruction.subsetWeight_mask line 1079
theorem OAI.TraceReconstruction.coordinateProduct_common_flags line 1084
def OAI.TraceReconstruction.schedulePayload line 1114
def OAI.TraceReconstruction.uniformSchedulePayload line 1118
theorem OAI.TraceReconstruction.hiddenSchedule_payload_exact line 1123
theorem OAI.TraceReconstruction.uniformSchedulePayload_steps line 1151
def OAI.TraceReconstruction.coordinateWord line 1169
theorem OAI.TraceReconstruction.coordinateWord_succ line 1171
theorem OAI.TraceReconstruction.coordinateWord_cons line 1175
theorem OAI.TraceReconstruction.coordinateProduct_simulates line 1180
theorem OAI.TraceReconstruction.sum_subset_choices line 1207
theorem OAI.TraceReconstruction.coordinateWord_pureAtomRun line 1215
theorem OAI.TraceReconstruction.uniform_schedule_word line 1220
theorem OAI.TraceReconstruction.lifting_count_scale line 1232
theorem OAI.TraceReconstruction.lifting_scale_valid line 1256
theorem OAI.TraceReconstruction.lifting_numeric_bound line 1267
theorem OAI.TraceReconstruction.maskLaw_simulates line 1293
theorem OAI.TraceReconstruction.uniformSchedulePayload_simulates line 1300

theorem OAI.TraceReconstruction.adjacent_power_lift line 1317

Source documentation

Explicit source common-part lifting, using finite auxiliary observations that decode exactly to ordinary complete traces of the adjacent pure powers.

theorem adjacent_power_lift {F k R : ℕ} {C p q : ℝ}
    (hk : 1≤k) (hR : 1≤R) (hp : p∈Set.Ioc 0 (1/8)) (hq : q∈Set.Icc 0 1)
    (hC : 1073741824≤p*C) (hF : C*k*R≤F)
    (P Q : FiniteLaw α) (f : α→List Bool) (w : List Bool)
    (hP : SimulatesTrace q P f (pureAtomRun w k))
    (hQ : SimulatesTrace q Q f (pureAtomRun w (k+1)))
    (hov : p≤FiniteLaw.overlap P Q) :
    ∃ (β : Type u) (_ : Fintype β) (P' Q' : FiniteLaw β) (g : β→List Bool),
      SimulatesTrace q P' g (pureAtomRun w (F*R)) ∧
      SimulatesTrace q Q' g (pureAtomRun w (F*R+R)) ∧
      (2/3:ℝ)≤FiniteLaw.overlap P' Q' := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.SimulatesTrace, OAI.TraceReconstruction.pureAtomRun, OAI.TraceReconstruction.FiniteLaw.overlap

theorem OAI.TraceReconstruction.FiniteLaw.tv_eq_positive_test line 1373

Source documentation

The maximizing test for total variation on a finite sample space.

theorem tv_eq_positive_test (P Q : FiniteLaw α) :
    P.tv Q = P.expect (fun a => if Q.mass a ≤ P.mass a then 1 else 0) -
      Q.expect (fun a => if Q.mass a ≤ P.mass a then 1 else 0) := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw

theorem OAI.TraceReconstruction.FiniteLaw.tv_le_of_tests line 1392
Source documentation
Dual characterization, sufficient for simulators with different latent spaces.
```
theorem tv_le_of_tests (P Q : FiniteLaw α) {E : ℝ}
    (h : ∀ f : α → ℝ, (∀ a, f a ∈ Set.Icc 0 1) →
      P.expect f-Q.expect f ≤ E) : P.tv Q ≤ E := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.FiniteLaw.abs_expect_sub_le_tv line 1398
def OAI.TraceReconstruction.listTraceLaw line 1411
Source documentation
The genuine complete-trace law embedded in a specified finite trace space. The extra elements have mass zero, not a cemetery mass.
```
def listTraceLaw (q : ℝ) (hq : q ∈ Set.Icc 0 1) (w : List Bool)
    (M : ℕ) (hw : w.length ≤ M) : FiniteLaw (BoundedTrace M) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.BoundedTrace
theorem OAI.TraceReconstruction.listTraceLaw_expect line 1417
theorem OAI.TraceReconstruction.listTraceLaw_simulates line 1426
def OAI.TraceReconstruction.listTraceOverlap line 1432
Source documentation
Ordinary overlap of complete traces, including unequal input lengths.
```
def listTraceOverlap (q : ℝ) (hq : q ∈ Set.Icc 0 1) (x y : List Bool) : ℝ :=
…
```

theorem OAI.TraceReconstruction.approximations_trace_tv line 1439

Source documentation

Common approximate simulation transfers distinguishability to genuine complete traces, without revealing the latent partition.

theorem approximations_trace_tv {α : Type*} [Fintype α]
    {q : ℝ} (hq : q ∈ Set.Icc 0 1) (P Q : FiniteLaw α) (decode : α → List Bool)
    (x y : List Bool) (Ex Ey : ℝ) (M : ℕ) (hx : x.length ≤ M) (hy : y.length ≤ M)
    (hP : ApproximatesTrace q P decode x Ex)
    (hQ : ApproximatesTrace q Q decode y Ey) :
    (listTraceLaw q hq x M hx).tv (listTraceLaw q hq y M hy) ≤ P.tv Q+Ex+Ey := by
…

Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.ApproximatesTrace, OAI.TraceReconstruction.listTraceLaw

structure OAI.TraceReconstruction.ConcreteLevelPair line 1476
Source documentation
A literal witness of the source level invariant. halfOrder is half its positive even moment order. countFactor is the prescribed upper multiplier C^(2*B*i+O_B(1)), to be instantiated uniformly in the actual construction. Finite outcomes suffice for the source's finite latent experiments, and any randomized common decoder can be included as an additional latent draw.
```
structure ConcreteLevelPair (q : ℝ) (hq : q ∈ Set.Icc 0 1)
    (N Δ d ω countFactor : ℝ) (i halfOrder : ℕ) where
…
```
def OAI.TraceReconstruction.FiniteLaw.joint line 1518
Source documentation
A joint law retaining both the latent variable and its conditional draw.
```
def joint (P : FiniteLaw α) (K : α → FiniteLaw β) : FiniteLaw (α × β) where
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
theorem OAI.TraceReconstruction.FiniteLaw.expect_joint line 1526
theorem OAI.TraceReconstruction.FiniteLaw.expect_mixture line 1530
theorem OAI.TraceReconstruction.FiniteLaw.mixture_eq_bind line 1535
theorem OAI.TraceReconstruction.FiniteLaw.coordinateProduct_map line 1539
Source documentation
Independent maps commute with the literal finite product law.
```
theorem coordinateProduct_map {n : ℕ} (P : Fin n → FiniteLaw α)
    (f : Fin n → α → β) :
    (coordinateProduct P).map (fun a i => f i (a i)) =
      coordinateProduct (fun i => (P i).map (f i)) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.FiniteLaw.map
theorem OAI.TraceReconstruction.FiniteLaw.pairedFlagLaw_map line 1567
Source documentation
Forgetting the report recovers the two independent side emissions.
```
theorem pairedFlagLaw_map (P Q H : FiniteLaw α) {ω : ℝ} (hω : 0 ≤ ω)
    (hP : ∀ a, ω*H.mass a ≤ P.mass a) (hQ : ∀ a, ω*H.mass a ≤ Q.mass a)
    (b : Bool) :
    (pairedFlagLaw P Q H hω hP hQ b).map Prod.snd = orientedProd P Q b := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.pairedFlagLaw, OAI.TraceReconstruction.FiniteLaw.map, OAI.TraceReconstruction.FiniteLaw.orientedProd
structure OAI.TraceReconstruction.PairedMechanisms line 1585
Source documentation
Data of the paired mechanisms, with common submass proved for each side. All words and their actual trace laws will be substituted in these fields.
```
structure PairedMechanisms (Side : Type*) [Fintype Side] (m : ℕ) where
…
```
abbrev OAI.TraceReconstruction.Reports line 1594
def OAI.TraceReconstruction.PairedMechanisms.reports line 1599
def OAI.TraceReconstruction.PairedMechanisms.reportsGiven line 1603
def OAI.TraceReconstruction.PairedMechanisms.fairOrientations line 1608
Source documentation
Bit orientations, prior to generating any emissions.
```
def fairOrientations (m : ℕ) : FiniteLaw (Fin m → Bool) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw
def OAI.TraceReconstruction.PairedMechanisms.orientationsGiven line 1613
Source documentation
Exact posterior, with zero-mass metadata treated by the same canonical formula. In particular unseen orientations are independent fair bits.
```
def orientationsGiven (z : Reports Side m) : FiniteLaw (Fin m → Bool) :=
…
```
Mentions: OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.FiniteLaw
def OAI.TraceReconstruction.PairedMechanisms.selectedLeafLaw line 1616
def OAI.TraceReconstruction.PairedMechanisms.orientationOracle line 1621
Source documentation
Actual orientation-first, unconditioned augmented observation.
```
def orientationOracle (P Q : FiniteLaw Leaf) (θ : (Fin m → Bool) → Fin n → Bool) :
    FiniteLaw (Reports Side m × (Fin n → Leaf)) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.Reports
def OAI.TraceReconstruction.PairedMechanisms.canonicalOracle line 1626
Source documentation
Metadata-first factorization of exactly the same law, not a new oracle.
```
def canonicalOracle (P Q : FiniteLaw Leaf) (θ : (Fin m → Bool) → Fin n → Bool) :
    FiniteLaw (Reports Side m × (Fin n → Leaf)) :=
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.Reports
theorem OAI.TraceReconstruction.PairedMechanisms.oracle_factorization line 1630
theorem OAI.TraceReconstruction.PairedMechanisms.canonicalOracle_density line 1649
Source documentation
The reference is independent old-first-law emissions, even after reporting all side traces. This equality is exact for every metadata value.
```
theorem canonicalOracle_density (P Q : FiniteLaw Leaf) (Z : Leaf → ℝ)
    (hZ : ∀ a, Q.mass a = P.mass a*(1+Z a))
    (θ : (Fin m → Bool) → Fin n → Bool) (z : Reports Side m) (x : Fin n → Leaf) :
    (M.canonicalOracle P Q θ).mass (z,x) =
      (M.reports.prod (P.product n)).mass (z,x) *
        averagedDensity (orientationsGiven z) θ Z x := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.Reports, OAI.TraceReconstruction.averagedDensity, OAI.TraceReconstruction.PairedMechanisms.orientationsGiven
theorem OAI.TraceReconstruction.PairedMechanisms.canonicalOracle_metadata line 1662
Source documentation
The full side metadata has a common law for both hypotheses.
```
theorem canonicalOracle_metadata (P Q : FiniteLaw Leaf)
    (θ : (Fin m → Bool) → Fin n → Bool) (F : Reports Side m → ℝ) :
    (M.canonicalOracle P Q θ).expect (fun z => F z.1) = M.reports.expect F := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.Reports
theorem OAI.TraceReconstruction.PairedMechanisms.reportsGiven_forget line 1670
Source documentation
Conditional on every orientation, forgetting flags gives independent side emissions. This is the unconditional simulation side of the construction.
```
theorem reportsGiven_forget (b : Fin m → Bool) :
    (M.reportsGiven b).map (fun z i => (z i).2) =
      FiniteLaw.coordinateProduct (fun i => FiniteLaw.orientedProd (M.first i) (M.second i) (b i)) := by
…
```
Mentions: OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.FiniteLaw.orientedProd