Probabilistic lens-ranges (Footprint)

The sub-probability analogue of DetermFootprint. A region of the state m is a set of sub-probability kernels m → SubProbability m, closed under Kleisli composition (*, with pure as identity — see the Monoid (m → SubProbability m) instance in GaudisCrypt.Language.SubProbability) and equal to its own double commutant.

The whole lattice/complement tower (Compl, from, PartialOrder, Lattice, BoundedOrder, compl_compl, CompleteLattice) is built purely from generic monoid–centralizer facts, so it mirrors DetermFootprint verbatim, only over the Kleisli monoid of kernels instead of Function.End. The genuinely probabilistic content — relating a ProgramDenotation to a Footprint — lives in ProgramDenotation.inFootprint and ProgramDenotation.footprint at the bottom of this file.

structure GaudisCrypt.Footprint (m : Type u_1) : Type u_1

• updates : Set (m → SubProbability m)
• id : pure ∈ self.updates
• comp {f g : m → SubProbability m} : f ∈ self.updates → g ∈ self.updates → f * g ∈ self.updates
• double_commutant : self.updates.centralizer.centralizer = self.updates

@[implicit_reducible]

instance GaudisCrypt.instComplFootprint {m : Type u_1} : Compl (Footprint m)

Equations

• GaudisCrypt.instComplFootprint = { compl := fun (range : GaudisCrypt.Footprint m) => { updates := range.updates.centralizer, id := ⋯, comp := ⋯, double_commutant := ⋯ } }

def GaudisCrypt.Footprint.from {m : Type u_1} (generators : Set (m → SubProbability m)) : Footprint m

Equations

• GaudisCrypt.Footprint.from generators = { updates := generators.centralizer.centralizer, id := ⋯, comp := ⋯, double_commutant := ⋯ }

@[simp]

theorem GaudisCrypt.Footprint.from_updates {m : Type u_1} (G : Set (m → SubProbability m)) : («from» G).updates = G.centralizer.centralizer

@[implicit_reducible]

instance GaudisCrypt.instPartialOrderFootprint {m : Type u_1} : PartialOrder (Footprint m)

Equations

• GaudisCrypt.instPartialOrderFootprint = { le := fun (x y : GaudisCrypt.Footprint m) => x.updates ≤ y.updates, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance GaudisCrypt.instLatticeFootprint {m : Type u_1} : Lattice (Footprint m)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GaudisCrypt.instBoundedOrderFootprint {m : Type u_1} : BoundedOrder (Footprint m)

Equations

• GaudisCrypt.instBoundedOrderFootprint = { top := { updates := ⊤, id := ⋯, comp := ⋯, double_commutant := ⋯ }, le_top := ⋯, bot := GaudisCrypt.Footprint.from ∅, bot_le := ⋯ }

theorem GaudisCrypt.Footprint.compl_antimono {m : Type u_1} {R S : Footprint m} (h : R ≤ S) : Sᶜ ≤ Rᶜ

The complement (commutant) is antitone.

theorem GaudisCrypt.Footprint.compl_compl {a : Type u_1} (x : Footprint a) : xᶜᶜ = x

theorem GaudisCrypt.Footprint.updates_eq_centralizer_compl {m : Type u_1} (R : Footprint m) : R.updates = (Submonoid.centralizer Rᶜ.updates).carrier

A range equals the centralizer of its own complement (double-commutant closure, stated with the commutant on the inside).

theorem GaudisCrypt.Footprint.from_le_iff {m : Type u_1} (G : Set (m → SubProbability m)) (R : Footprint m) : «from» G ≤ R ↔ G ⊆ R.updates

Galois connection for from: from G is the smallest range whose updates contain G. Since R is double-commutant-closed, from G ≤ R iff G ⊆ R.updates.

@[implicit_reducible]

instance GaudisCrypt.instCompleteSemilatticeSupFootprint {m : Type u_1} : CompleteSemilatticeSup (Footprint m)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GaudisCrypt.instCompleteSemilatticeInfFootprint {m : Type u_1} : CompleteSemilatticeInf (Footprint m)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GaudisCrypt.instCompleteLatticeFootprint {m : Type u_1} : CompleteLattice (Footprint m)

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.Footprint.from_mono {m : Type u_1} {G G' : Set (m → SubProbability m)} (h : G ⊆ G') : «from» G ≤ «from» G'

noncomputable def GaudisCrypt.Lens.liftSubProbability {a b : Type} (lens : Lens a b) (κ : a → SubProbability a) (x : b) : SubProbability b

Equations

• lens.liftSubProbability κ x = do let a_1 ← κ (lens.get x) pure (lens.set a_1 x)

noncomputable def GaudisCrypt.Lens.liftFootprint {a b : Type} (lens : Lens a b) (range : Footprint a) : Footprint b

Equations

• lens.liftFootprint range = GaudisCrypt.Footprint.from (lens.liftSubProbability '' range.updates)

theorem GaudisCrypt.Lens.liftFootprint_mono {a b : Type} (lens : Lens a b) {r r' : Footprint a} (h : r ≤ r') : lens.liftFootprint r ≤ lens.liftFootprint r'

Programs and probabilistic ranges

def GaudisCrypt.ProgramDenotation.inFootprint {s a : Type} (p : ProgramDenotation s a) (R : Footprint s) : Prop

A program p lies in the probabilistic range R iff it commutes with every kernel outside R (i.e. in the commutant Rᶜ): running an outside kernel f on the state and then p is the same as running p and then f on the resulting state. This is the sub-probability analogue of ProgramDenotation.inRange.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GaudisCrypt.ProgramDenotation.footprintUnit {s : Type} (p : ProgramDenotation s Unit) : Footprint s

The probabilistic range of a Unit-returning program: the Footprint generated by its single induced state kernel (run p, forget the result). Ported from the rangeUnit2 sketch in Language/Semantics.lean.

Equations

• p.footprintUnit = GaudisCrypt.Footprint.from {fun (st : s) => do let __discr ← p st match __discr with | (fst, st') => pure st'}

noncomputable def GaudisCrypt.ProgramDenotation.footprint {s a : Type} (p : ProgramDenotation s a) : Footprint s

The probabilistic range of a program p : ProgramDenotation s a: the Footprint generated by the family of return-value-conditioned state kernels. For each possible return value y : a, the kernel runs p, keeps only the mass that returns y (killing the rest with ⊥), and forgets the result, leaving a kernel s → SubProbability s. Indexing by y records how the final state correlates with what p returns. Ported from the range2 sketch in Language/Semantics.lean.

Equations

• p.footprint = GaudisCrypt.Footprint.from (Set.range fun (y : a) (st : s) => do let __discr ← p st match __discr with | (x, st') => if x = y then pure st' else ⊥)

Litmus test: p.inFootprint R ↔ p.footprint ≤ R

The probabilistic analogue of the bicommutant litmus test. The key device is the return-value slice projK y: post-composing a kernel into a × s with projK y keeps only the mass that returns y and projects to the state. Slicing turns the joint commutation equation defining inFootprint into per-y commutations of the conditioned kernels kᵧ (the generators of footprint) with the commutant Rᶜ, i.e. kᵧ ∈ centralizer Rᶜ = R.updates. The forward direction is pure slicing; the backward direction reassembles the joint kernel from its slices, which needs the return type a to be Countable.

theorem GaudisCrypt.ProgramDenotation.footprint_le_of_inFootprint {s a : Type} {p : ProgramDenotation s a} {R : Footprint s} (h : p.inFootprint R) : p.footprint ≤ R

Litmus test, forward (soundness): if p commutes with the commutant Rᶜ, its constructive footprint is contained in R. No countability needed — this is pure slicing of the commutation equation.

theorem GaudisCrypt.ProgramDenotation.inFootprint_of_footprint_le {s a : Type} {p : ProgramDenotation s a} {R : Footprint s} (h : p.footprint ≤ R) : p.inFootprint R

Litmus test, backward (completeness): if p's constructive footprint is contained in R, then p commutes with the commutant Rᶜ. Countability-free (subtask 4): the joint kernel is reassembled from its slices via the discreteness invariant (ext_of_slices), not from countability of the return type.

theorem GaudisCrypt.ProgramDenotation.inFootprint_iff_footprint_le {s a : Type} {p : ProgramDenotation s a} {R : Footprint s} : p.inFootprint R ↔ p.footprint ≤ R

Litmus test: a program lies in the range R (commutes with the commutant) iff its constructive footprint is ≤ R. Ported from the Litmus test note in Language/Semantics.lean.

Closure properties of inFootprint / footprint

theorem GaudisCrypt.inFootprint_iff_clean {s c : Type} {P : ProgramDenotation s c} {R : Footprint s} : P.inFootprint R ↔ ∀ f ∈ Rᶜ.updates, (fun (st : s) => f st >>= P) = fun (st : s) => do let w ← P st let st'' ← f w.2 pure (w.1, st'')

Clean reformulation of inFootprint: strip the trailing pure-repack from the "run outside-kernel first" side via bind_pure.

theorem GaudisCrypt.ProgramDenotation.inFootprint_mono {s c : Type} {P : ProgramDenotation s c} {R R' : Footprint s} (h : P.inFootprint R) (hR : R ≤ R') : P.inFootprint R'

Monotonicity: a larger range still contains the program.

theorem GaudisCrypt.ProgramDenotation.inFootprint_bind {s a b : Type} {p : ProgramDenotation s a} {q : a → ProgramDenotation s b} {R : Footprint s} (hp : p.inFootprint R) (hq : ∀ (x : a), (q x).inFootprint R) : (p >>= q).inFootprint R

Commutation composes through bind: if p and every q x commute with the commutant Rᶜ, so does p >>= q. Pure Kleisli algebra — no countability needed. The slogan is pre/post (run-f-first / run-f-last) compose via bind_assoc, and the hypotheses swap pre ↔ post at p and at each q x.

theorem GaudisCrypt.ProgramDenotation.footprint_bind_le {s a b : Type} (p : ProgramDenotation s a) (q : a → ProgramDenotation s b) : (p >>= q).footprint ≤ p.footprint ⊔ ⨆ (x : a), (q x).footprint

Range of a bind: (p >>= q).footprint ≤ p.footprint ⊔ ⨆ x, (q x).footprint. The footprint of a sequenced computation is contained in p's footprint together with the union of the continuations' footprints. Countability-free (subtask 4): the self-range step (inFootprint_of_footprint_le) no longer needs countable return types.

Parity primitives: Lens.footprint and primitive ranges

The probabilistic analogues of Lens.range / ProgramDenotation.inRange_pure/set/get, mirroring the DetermFootprint leaves so consumers can migrate. A deterministic state update embeds as a Dirac kernel via diracKer; Lens.footprint is generated by the lens-localized ones.

noncomputable def GaudisCrypt.diracKer {s : Type} (f : Function.End s) : s → SubProbability s

A deterministic state update f : Function.End s as a Dirac kernel. The Kleisli embedding Function.End s ↪ (s → SubProbability s).

Equations

• GaudisCrypt.diracKer f st = pure (f st)

def GaudisCrypt.Footprint.orbit_setoid {m : Type} (R : Footprint m) : Setoid m

The R-orbit equivalence on m: s ~ s' iff s' is reachable from s via the deterministic updates of R — Dirac kernels diracKer f ∈ R.updates. The Footprint analogue of DetermFootprint.orbit_setoid.

Equations

• R.orbit_setoid = { r := Relation.EqvGen fun (s s' : m) => ∃ (f : Function.End m), GaudisCrypt.diracKer f ∈ R.updates ∧ f s = s', iseqv := ⋯ }

def GaudisCrypt.Footprint.global_getter {m : Type} (R : Footprint m) : Getter (Quotient R.orbit_setoid) m

The "global getter" of a Footprint: the quotient projection onto R-orbit classes. Two states read equal iff they lie in the same R-orbit (differ only within R).

Equations

• R.global_getter = { get := Quotient.mk R.orbit_setoid }

def GaudisCrypt.Footprint.touched_getter {m : Type} (R : Footprint m) : Getter (Quotient Rᶜ.orbit_setoid) m

The "touched" getter: global_getter of the commutant Rᶜ. Two states read equal iff they differ only in Rᶜ — i.e. they agree on the content R owns. For R = fvP_proc A this is glob A (EasyCrypt's ={glob A} is exactly touched_getter x = touched_getter y).

Equations

• R.touched_getter = Rᶜ.global_getter

theorem GaudisCrypt.Footprint.touched_getter_get_eq_of_mem {m : Type} {R : Footprint m} {f : Function.End m} (hf : diracKer f ∈ Rᶜ.updates) (σ : m) : R.touched_getter.get (f σ) = R.touched_getter.get σ

A single deterministic Rᶜ-update cannot move the touched getter: f σ and σ lie in the same Rᶜ-orbit. The pointwise engine for "={glob A} is preserved by writes outside A's footprint" (e.g. oracle writes, for an oracle-disjoint A).

def GaudisCrypt.Footprint.HasReset {m : Type} (S : Footprint m) (σ : m) : Prop

A Footprint S is resettable at σ if it admits an S-update that overwrites its own content (S.touched_getter) with σ's value while fixing σ. This is the "S is a genuine, overwritable memory region" property: every lens footprint has it (Lens.footprint_hasReset), an abelian bicommutant one need not. It is the frame's faithfulness witness, living on the (lens-derived) oracle region rather than on the adversary.

Equations

• S.HasReset σ = ∃ (f : Function.End m), GaudisCrypt.diracKer f ∈ S.updates ∧ f σ = σ ∧ ∀ (s : m), S.touched_getter.get (f s) = S.touched_getter.get σ

Observational indistinguishability through a footprint

An R-test observes a state by running one R-update and reading off its acceptance probability — the total weight SubProbability.mass of the result. Footprint.indistinguishable is the induced observational equivalence: no R-test separates the two states (indistinguishable_iff_testsOf). The touched getter is sound for it (indistinguishable_of_touched_getter_eq): states agreeing on the content R owns pass every R-test with the same probability. (Tests comparing the weight against an interval rather than a single value separate exactly as well as the exact-weight ones formalized here.)

def GaudisCrypt.Footprint.indistinguishable {m : Type u_1} (R : Footprint m) (σ σ' : m) : Prop

Two states are indistinguishable through R when every update of R accepts both with the same total weight (SubProbability.mass).

Equations

• R.indistinguishable σ σ' = ∀ h ∈ R.updates, (h σ).mass = (h σ').mass

theorem GaudisCrypt.Footprint.indistinguishable_equivalence {m : Type u_1} (R : Footprint m) : Equivalence R.indistinguishable

Footprint.indistinguishable is an equivalence relation.

theorem GaudisCrypt.Footprint.indistinguishable.anti {m : Type u_1} {R S : Footprint m} {σ σ' : m} (h : S.indistinguishable σ σ') (hRS : R ≤ S) : R.indistinguishable σ σ'

Footprint.indistinguishable is antitone in the footprint: a larger footprint has more tests, hence a finer indistinguishability.

def GaudisCrypt.Footprint.testsOf {m : Type u_1} (R : Footprint m) : Set (m → Prop)

The tests of a footprint: the state predicates decided by comparing the acceptance probability of a single R-update against a fixed weight.

Equations

• R.testsOf = {g : m → Prop | ∃ h ∈ R.updates, ∃ (r : NNReal), ∀ (σ : m), g σ ↔ (h σ).mass = r}

theorem GaudisCrypt.Footprint.indistinguishable_iff_testsOf {m : Type u_1} (R : Footprint m) (σ σ' : m) : R.indistinguishable σ σ' ↔ ∀ g ∈ R.testsOf, g σ ↔ g σ'

Indistinguishability is exactly "passing the same tests".

theorem GaudisCrypt.Footprint.indistinguishable_of_touched_getter_eq {m : Type} {R : Footprint m} {σ σ' : m} (hg : R.touched_getter.get σ = R.touched_getter.get σ') : R.indistinguishable σ σ'

Soundness of the touched getter for tests: states with equal R-owned content (equal R.touched_getter — EasyCrypt's ={glob}) are indistinguishable through R. Each Rᶜ-orbit step is a deterministic outside update; every R-update commutes with it (the centralizer equation), and deterministic post-composition preserves mass (SubProbability.mass_bind_dirac).

noncomputable def GaudisCrypt.Lens.footprint {a s : Type} (lens : Lens a s) : Footprint s

The probabilistic range of a lens: generated by the Dirac kernels of its localized deterministic updates lens.liftFunction g. The sub-probability analogue of Lens.range.

Equations

• lens.footprint = GaudisCrypt.Footprint.from (Set.range lens.liftSubProbability)

theorem GaudisCrypt.Lens.liftSubProbability_diracKer {a s : Type} (lens : Lens a s) (g : Function.End a) : lens.liftSubProbability (diracKer g) = diracKer (lens.liftFunction g)

Lifting a Dirac kernel along a lens is the Dirac kernel of the lifted function.

theorem GaudisCrypt.Lens.diracKer_liftFunction_mem_footprint {a s : Type} (lens : Lens a s) (g : Function.End a) : diracKer (lens.liftFunction g) ∈ lens.footprint.updates

diracKer (lens.liftFunction g) is a lens.footprint generator: it equals lens.liftSubProbability (diracKer g), hence lies in lens.footprint.updates.

theorem GaudisCrypt.inFootprint_subprob {s a : Type} {p : ProgramDenotation s a} {R : Footprint s} (h : p.inFootprint R) {f : s → s} (hf : diracKer f ∈ Rᶜ.updates) (σ : s) : p (f σ) = do let xs ← p σ pure (xs.1, f xs.2)

Kernel-shift extraction: a program in range R commutes with a deterministic outside-update f (as a Dirac kernel). The inFootprint analogue of ProgramDenotation.inRange_subprob.

theorem GaudisCrypt.ProgramDenotation.set_apply {a s : Type} (v : Lens a s) (x : a) (st : s) : set v x st = pure ((), v.set x st)

ProgramDenotation.set v x applied at a state: a deterministic write.

theorem GaudisCrypt.ProgramDenotation.get_apply {a s : Type} (v : Lens a s) (st : s) : get v st = pure (v.get st, st)

ProgramDenotation.get v applied at a state: a read leaving the state unchanged.

theorem GaudisCrypt.ProgramDenotation.inFootprint_pure {s a : Type} (x : a) (R : Footprint s) : (pure x).inFootprint R

pure x is in every probabilistic range — it touches no state.

theorem GaudisCrypt.ProgramDenotation.inFootprint_set {a s : Type} (v : Lens a s) (x : a) : (set v x).inFootprint v.footprint

ProgramDenotation.set v x lives in v.footprint.

theorem GaudisCrypt.ProgramDenotation.inFootprint_get {a s : Type} (v : Lens a s) : (get v).inFootprint v.footprint

ProgramDenotation.get v lives in v.footprint: it reads v, never writes. The extraction hstar says any commutant kernel f preserves v.get almost surely.

theorem GaudisCrypt.diracKer_mul {s : Type} (p q : Function.End s) : diracKer p * diracKer q = diracKer (p * q)

diracKer is a monoid homomorphism Function.End s → (s → SubProbability s).

theorem GaudisCrypt.bind_swap {s α γ : Type} (ν : SubProbability s) (μ : SubProbability α) (k : α → s → SubProbability γ) : (do let st' ← ν let a ← μ k a st') = do let a ← μ let st' ← ν k a st'

Commute two binds — a Fubini swap for sub-probability kernels.

theorem GaudisCrypt.Lens.liftSubProbability_comm_of_disjoint {a b s : Type} (v : Lens a s) (L : Lens b s) [hd : disjoint v L] (κ : a → SubProbability a) (ρ : b → SubProbability b) : v.liftSubProbability κ * L.liftSubProbability ρ = L.liftSubProbability ρ * v.liftSubProbability κ

Disjoint lenses' localized kernels commute (Fubini via bind_swap).

theorem GaudisCrypt.Lens.footprint_le_compl_of_disjoint {a b s : Type} (v : Lens a s) (L : Lens b s) [hd : disjoint v L] : v.footprint ≤ L.footprintᶜ

Disjoint lenses have ranges in each other's complements: disjoint v L gives v.footprint ≤ (L.footprint)ᶜ.

theorem GaudisCrypt.Lens.footprint_hasReset {c m : Type} (l : Lens c m) (σ : m) : l.footprint.HasReset σ

Every lens footprint is resettable — the probabilistic HasReset analogue of Lens.range_hasOrbitCollapse. The reset is the lens overwrite l.set (l.get σ); it lands every state in σ's (l.footprint)ᶜ-orbit, so touched_getter collapses to σ's value.

theorem GaudisCrypt.Lens.footprint_eq_bot_of_subsingleton {a s : Type} [Subsingleton a] (l : Lens a s) : l.footprint = ⊥

A lens with subsingleton content has trivial footprint. Its localized kernels can only resample the unique content value, so they are scaled identities — central in the kernel monoid, hence inside every footprint, in particular ⊥.

theorem GaudisCrypt.Lens.footprint_eq_bot_of_le_compl {a s : Type} (l : Lens a s) (h : l.footprint ≤ l.footprintᶜ) : l.footprint = ⊥

A lens footprint inside its own commutant is trivial. Self-commutation makes any two constant writes commute, which (evaluated at a state and read back through the lens) forces all content values to coincide — so the content is a subsingleton and Lens.footprint_eq_bot_of_subsingleton applies.

theorem GaudisCrypt.Lens.footprint_touched_getter_eq_iff {c m : Type} (l : Lens c m) (x y : m) : l.footprint.touched_getter.get x = l.footprint.touched_getter.get y ↔ l.get x = l.get y

A lens footprint's touched content is its lens getter. For a lens l, the opaque orbit quotient (l.footprint).touched_getter collapses to l.get: two states have equal touched content iff they agree on l.get. Lets glob endpoints state their premises via the concrete l.get instead of the quotient.

theorem GaudisCrypt.Footprint.touchedGetter_is_getter {s a : Type} [Nonempty s] (lens : Lens a s) : ∃ (f : Quotient lens.footprintᶜ.orbit_setoid ≃ a), f.toFun ∘ lens.footprint.touched_getter.get = lens.get

theorem GaudisCrypt.Lens.footprint_compl_touched_getter_eq_iff {c m : Type} (l : Lens c m) (x y : m) : l.footprintᶜ.touched_getter.get x = l.footprintᶜ.touched_getter.get y ↔ l.compl.get x = l.compl.get y

A lens footprint's complement touched content is the complement lens's getter. For a lens l, ((l.footprint)ᶜ).touched_getter collapses to l.compl.get: two states have equal outside-l content iff they agree on l.compl.get. The Oᶜ companion of Lens.footprint_touched_getter_eq_iff (folds in compl_compl).

The lens converse: tests recover the lens content

For a lens footprint the observational equivalence coincides with the touched getter: the conditional abort Lens.testKer l x₀ (keep the state iff the lens reads x₀) lies in l.footprint — it commutes with everything commuting with the lens writes — and its acceptance mass reads the lens. So Footprint.indistinguishable pins the lens content exactly: this is the tomography converse of Footprint.indistinguishable_of_touched_getter_eq, which CounterExamples/IndistinguishableVsGlob.lean shows fails for general (abelian) footprints.

noncomputable def GaudisCrypt.Lens.testKer {a s : Type} (l : Lens a s) (x₀ : a) : s → SubProbability s

The conditional-abort test of a lens at x₀: keep the state if the lens reads x₀, abort otherwise. Acceptance probability = "the lens reads x₀".

Equations

• l.testKer x₀ σ = if l.get σ = x₀ then pure σ else ⊥

theorem GaudisCrypt.Lens.testKer_mem_footprint {a s : Type} (l : Lens a s) (x₀ : a) : l.testKer x₀ ∈ l.footprint.updates

The conditional abort is an honest l-test: it lies in the lens footprint. It commutes with any kernel k commuting with the constant writes, because such a k satisfies k σ >>= (pure ∘ l.set c) = k (l.set c σ) — its output's l-content is pinned by a write — so the abort filter passes k's output through untouched (accept branch) or kills it entirely (reject branch).

theorem GaudisCrypt.Lens.get_eq_of_indistinguishable {a s : Type} {l : Lens a s} {σ σ' : s} (h : l.footprint.indistinguishable σ σ') : l.get σ = l.get σ'

Tests recover the lens content: states indistinguishable through a lens footprint have equal lens reads — apply the conditional abort at l.get σ.

theorem GaudisCrypt.Lens.footprint_indistinguishable_iff_touched_getter_eq {a s : Type} (l : Lens a s) (σ σ' : s) : l.footprint.indistinguishable σ σ' ↔ l.footprint.touched_getter.get σ = l.footprint.touched_getter.get σ'

On lens footprints the two notions agree: observational indistinguishability = equal touched getter (= equal lens content, via Lens.footprint_touched_getter_eq_iff). This is the tomography converse that fails for general footprints — for a genuine memory region, what the tests see is exactly what the getter reads.

theorem GaudisCrypt.Lens.footprint_indistinguishable_iff_get_eq {a s : Type} (l : Lens a s) (σ σ' : s) : l.footprint.indistinguishable σ σ' ↔ l.get σ = l.get σ'

The lens-content form of the agreement.

theorem GaudisCrypt.Footprint.indistinguishable_iff_touched_getter_eq_of_eq_lens {a m : Type} {R : Footprint m} {l : Lens a m} (hR : R = l.footprint) (σ σ' : m) : R.indistinguishable σ σ' ↔ R.touched_getter.get σ = R.touched_getter.get σ'

The agreement transfers along an identification of a footprint with a lens region — the form consumed for syntactic adversaries, whose assigned region (FVP.fvP_proc) is a variable (lens) region.

theorem GaudisCrypt.Footprint.get_eq_of_indistinguishable_of_testKer_mem {a m : Type} {R : Footprint m} {l : Lens a m} (htest : ∀ (x₀ : a), l.testKer x₀ ∈ R.updates) {σ σ' : m} (h : R.indistinguishable σ σ') : l.get σ = l.get σ'

Tests pin the lens content pointwise: any footprint merely containing the conditional-abort tests of l (not necessarily all of l.footprint) already separates states by l.get.

theorem GaudisCrypt.Footprint.touched_getter_eq_of_le {m : Type} {R S : Footprint m} (h : R ≤ S) {σ σ' : m} (hg : S.touched_getter.get σ = S.touched_getter.get σ') : R.touched_getter.get σ = R.touched_getter.get σ'

touched_getter equality is antitone in the footprint: a smaller footprint has a coarser touched getter, so S-touched equality descends to R-touched equality along R ≤ S.

theorem GaudisCrypt.Footprint.indistinguishable_iff_touched_getter_eq_of_sandwich {a m : Type} {R : Footprint m} {l : Lens a m} (htest : ∀ (x₀ : a), l.testKer x₀ ∈ R.updates) (hle : R ≤ l.footprint) (σ σ' : m) : R.indistinguishable σ σ' ↔ R.touched_getter.get σ = R.touched_getter.get σ'

Pointwise sandwich agreement: for a footprint R that (i) contains l's tests and (ii) is bounded by l's region, indistinguishability through R is touched-getter equality — no identification R = l.footprint needed. This is the form for syntactic over-approximations (FVP.fvP_proc): (ii) is the standard upper-bound computation, and (i) is a single generator membership (the reduced read-slices are the tests).

Disjointness bridge

theorem GaudisCrypt.ProgramDenotation.set_inFootprint_compl_of_disjoint {a b s : Type} (v : Lens a s) (L : Lens b s) [disjoint v L] (x : a) : (set v x).inFootprint L.footprintᶜ

ProgramDenotation.set v x lives in L.footprintᶜ when v is disjoint from L.

theorem GaudisCrypt.ProgramDenotation.get_inFootprint_compl_of_disjoint {a b s : Type} (v : Lens a s) (L : Lens b s) [disjoint v L] : (get v).inFootprint L.footprintᶜ

ProgramDenotation.get v lives in L.footprintᶜ when v is disjoint from L.

Sampling: ProgramDenotation.uniform

ProgramDenotation.uniform lives in the trivial range ⊥ — it samples a value without touching the state. Because ⊥ᶜ = univ, this means it commutes with every kernel, which is a Fubini swap between the sampling and an arbitrary state-kernel. The swap (bind_swap) is countability-free (subtask 4): it goes through the discreteness invariant, so neither the sampled type nor the (possibly uncountable) state need be countable.

theorem GaudisCrypt.ProgramDenotation.inFootprint_uniform {s α : Type} [Fintype α] [Nonempty α] : uniform.inFootprint ⊥

ProgramDenotation.uniform lives in the trivial range ⊥ — it samples a value, touching no state. Needs only Fintype α (the sampled type), not countability of the state.

Localized kernels lie in the lens's range

theorem GaudisCrypt.Mlocalized_in_footprint {c s : Type} (M : Lens c s) (ρ : c → SubProbability c) : (fun (st : s) => do let mc' ← ρ (M.get st) pure (M.set mc' st)) ∈ M.footprint.updates

An M-localized kernel lies in M.footprint. A kernel that reads only M.get, samples a new M-value, and writes it back (ρ (M.get st) >>= fun mc' => pure (M.set mc' st)) commutes with the commutant M.footprintᶜ — using that any such f preserves M.get a.s. and commutes with M.set, plus the Fubini swap bind_swap (countability-free since subtask 4).

Disjoint programs commute (no orbit machinery)

Programs with disjoint probabilistic ranges can be run in either order with the same joint (output, state) distribution. Unlike the DetermFootprint version (commute_of_disjoint, which needs HasOrbitCollapse preconditions and [Countable s]), this follows directly from the constructive footprint + litmus: slicing the joint by the return value (x₀, y₀) collapses each side to a product of the return-conditioned kernels kp/kq, which commute because they live in the disjoint ranges R, R'. After subtask 4 this needs no countability at all — neither the state s nor the return types — since slice-reassembly (ext_of_slices) goes through the discreteness invariant.

theorem GaudisCrypt.ProgramDenotation.commute_of_disjoint_footprint {s a b : Type} {p : ProgramDenotation s a} {q : ProgramDenotation s b} {R R' : Footprint s} (hp : p.inFootprint R) (hq : q.inFootprint R') (hdisj : R ≤ R'ᶜ) : (do let x ← p let y ← q pure (x, y)) = do let y ← q let x ← p pure (x, y)

Disjoint programs commute. If p lives in R, q in R', and R ≤ R'ᶜ, then p and q may be run in either order with the same (output, state) distribution. The probabilistic analogue of ProgramDenotation.commute_of_disjoint — but with no HasOrbitCollapse hypotheses and, after subtask 4, no countability whatsoever (the joint kernel is reassembled from its slices via the discreteness invariant, not from countable state or return types).

theorem GaudisCrypt.ProgramDenotation.commute_of_disjoint_footprint_lens {s a b c d : Type} {p : ProgramDenotation s a} {q : ProgramDenotation s b} {l : Lens c s} {l' : Lens d s} (hp : p.inFootprint l.footprint) (hq : q.inFootprint l'.footprint) (hdisj : l.footprint ≤ l'.footprintᶜ) : (do let x ← p let y ← q pure (x, y)) = do let y ← q let x ← p pure (x, y)

Lens-range specialisation of commute_of_disjoint_footprint. A thin wrapper (no HasOrbitCollapse to discharge, unlike the DetermFootprint commute_of_disjoint_lens), matching that API for drop-in migration.

theorem GaudisCrypt.ProgramDenotation.commute_of_disjoint_lenses {s a b c d : Type} {p : ProgramDenotation s a} {q : ProgramDenotation s b} {l : Lens c s} {l' : Lens d s} [disjoint l l'] (hp : p.inFootprint l.footprint) (hq : q.inFootprint l'.footprint) : (do let x ← p let y ← q pure (x, y)) = do let y ← q let x ← p pure (x, y)

When the lenses l, l' are disjoint, the disjointness of their probabilistic ranges is automatic (Lens.footprint_le_compl_of_disjoint), so the caller supplies only the two inFootprint confinement proofs.

Corollaries: disjoint reads/writes commute

End-to-end payoff of the toolkit — the primitives (inFootprint_set/get) feed straight into commute_of_disjoint_lenses, so independent operations on disjoint lenses may be reordered.

theorem GaudisCrypt.ProgramDenotation.set_set_commute_of_disjoint {s γ δ : Type} (l : Lens γ s) (l' : Lens δ s) [disjoint l l'] (x : γ) (y : δ) : (do let a ← set l x let b ← set l' y pure (a, b)) = do let b ← set l' y let a ← set l x pure (a, b)

Two writes to disjoint lenses commute.

theorem GaudisCrypt.ProgramDenotation.get_set_commute_of_disjoint {s γ δ : Type} (l : Lens γ s) (l' : Lens δ s) [disjoint l l'] (y : δ) : (do let a ← get l let b ← set l' y pure (a, b)) = do let b ← set l' y let a ← get l pure (a, b)

A read and a write to disjoint lenses commute.

theorem GaudisCrypt.ProgramDenotation.get_get_commute_of_disjoint {s γ δ : Type} (l : Lens γ s) (l' : Lens δ s) [disjoint l l'] : (do let a ← get l let b ← get l' pure (a, b)) = do let b ← get l' let a ← get l pure (a, b)

Two reads of disjoint lenses commute.

while_loop confinement (fixpoint)

A while loop whose guard and body are confined to R is itself confined to R. The loop is the least fixpoint of while_iteration; each Kleene iterate is confined and confinement is closed under ω-suprema of chains.

theorem GaudisCrypt.inFootprint_bot {s a : Type} (R : Footprint s) : ⊥.inFootprint R

⊥ (the always-diverging program) lies in every footprint: it commutes with all kernels.

theorem GaudisCrypt.inFootprint_sideL_cont {s a : Type} (f : s → SubProbability s) : OmegaCompletePartialOrder.ωScottContinuous fun (p : ProgramDenotation s a) (st : s) => do let st' ← f st p st'

The "run outside kernel first" side of the inFootprint equation, as a map of the program p, is ω-Scott-continuous (rewritten as a ProgramDenotation bind so bind_ωScottContinuous applies).

theorem GaudisCrypt.inFootprint_sideR_cont {s a : Type} (f : s → SubProbability s) : OmegaCompletePartialOrder.ωScottContinuous fun (p : ProgramDenotation s a) (st : s) => do let w ← p st let st'' ← f w.2 pure (w.1, st'')

The "run outside kernel last" side of the inFootprint equation is ω-Scott-continuous.

theorem GaudisCrypt.inFootprint_ωSup {s a : Type} (R : Footprint s) (c : OmegaCompletePartialOrder.Chain (ProgramDenotation s a)) (hc : ∀ (n : ℕ), (c n).inFootprint R) : (OmegaCompletePartialOrder.ωSup c).inFootprint R

inFootprint R is closed under ω-suprema of chains. Both sides of the clean commutation equation are ω-Scott-continuous in the program, so if every chain element self-commutes, the supremum does too — the admissibility needed for the while_loop fixpoint.

theorem GaudisCrypt.while_iter_inFootprint {s : Type} (R : Footprint s) (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) (hcond : cond.inFootprint R) (hbody : body.inFootprint R) (g : Unit → ProgramDenotation s Unit) (hg : (g ()).inFootprint R) : ((while_iteration cond body) g ()).inFootprint R

One unrolling of the while_iteration operator preserves inFootprint R (given the guard and body do).

theorem GaudisCrypt.while_loop_inFootprint {s : Type} (R : Footprint s) (cond : ProgramDenotation s Bool) (body : ProgramDenotation s Unit) (hcond : cond.inFootprint R) (hbody : body.inFootprint R) : (while_loop cond body).inFootprint R

while_loop confinement. A while loop whose guard and body are confined to R is itself confined to R. The loop is the least fixpoint ⨆ₙ Fⁿ⊥ of while_iteration; each Kleene iterate is confined (inFootprint_bot/while_iter_inFootprint), and inFootprint_ωSup passes this to the supremum.

Reconstructing lenses from footprints

def GaudisCrypt.Footprint.FromLens {s : Type} (F : Footprint s) : Prop

Equations

• F.FromLens = ∃ (l : GaudisCrypt.Lens (Quotient Fᶜ.orbit_setoid) s), F = l.footprint

noncomputable def GaudisCrypt.Footprint.FromLens.lens {s : Type} {F : Footprint s} (h : F.FromLens) : Lens (Quotient Fᶜ.orbit_setoid) s

Equations

• h.lens = Classical.choose h

theorem GaudisCrypt.Lens.liftSubProbability_chain {a b c : Type} {lens1 : Lens a b} {lens2 : Lens b c} : (lens2.chain lens1).liftSubProbability = lens2.liftSubProbability ∘ lens1.liftSubProbability

theorem GaudisCrypt.Lens.liftFootprint_top {a b : Type} (lens : Lens a b) : lens.liftFootprint ⊤ = lens.footprint

Lifting the top footprint through a lens recovers the lens's own footprint.

@[simp]

theorem GaudisCrypt.Lens.id_footprint {s : Type} : id.footprint = ⊤

theorem GaudisCrypt.Lens.bijection_footprint {a b : Type} (e : a ≃ b) : (bijection e).footprint = ⊤

A bijection lens touches all of the state: its footprint is ⊤. Every kernel k is the lift of its e-conjugate, so the generators already exhaust the kernel monoid.

theorem GaudisCrypt.Footprint.eq_of_isEmpty {m : Type} [IsEmpty m] (R S : Footprint m) : R = S

Over an empty state type every footprint coincides: the only update kernel is pure.

Corner / slice machinery (relocated from FV.lean)

noncomputable def GaudisCrypt.Lens.reduceSubProbability {a b : Type} (lens : Lens a b) (p : (b → SubProbability b) × (Unit → SubProbability lens.ComplContent) × (lens.ComplContent → SubProbability Unit)) : a → SubProbability a

Given a joint kernel f on a × b, an input distribution i on b, and a weighting o on the b-output, produce the a-kernel that feeds i, runs f, and weights/discards the b-component via o.

Equations

• lens.reduceSubProbability p m = do let m' ← p.2.1 () let m'' ← p.1 (lens.splitSpace.invFun (m, m')) let __discr ← p.2.2 (lens.compl.get m'') have x : Unit := __discr pure (lens.get m'')

@[simp]

theorem GaudisCrypt.Lens.splitSpace_invFun_get {a : Type u_1} {b : Type u_2} (lens : Lens a b) (m : a) (c : lens.ComplContent) : lens.get (lens.splitSpace.invFun (m, c)) = m

Reading the focus of a reconstructed state recovers the focus component.

theorem GaudisCrypt.Lens.splitSpace_invFun_compl_get {a : Type u_1} {b : Type u_2} (lens : Lens a b) (m : a) (c : lens.ComplContent) : lens.compl.get (lens.splitSpace.invFun (m, c)) = c

Reading the complement of a reconstructed state recovers the complement component.

theorem GaudisCrypt.Lens.splitSpace_invFun_set {a : Type u_1} {b : Type u_2} (lens : Lens a b) (m a' : a) (c : lens.ComplContent) : lens.set a' (lens.splitSpace.invFun (m, c)) = lens.splitSpace.invFun (a', c)

Overwriting the focus of a reconstructed state is the same as reconstructing with a new focus.

@[simp]

theorem GaudisCrypt.Lens.compl_get_set {a : Type u_1} {b : Type u_2} (lens : Lens a b) (a' : a) (x : b) : lens.compl.get (lens.set a' x) = lens.compl.get x

Overwriting the focus leaves the complement class unchanged.

theorem GaudisCrypt.Lens.reduceSubProbability_mul_left {a b : Type} (lens : Lens a b) (f : b → SubProbability b) (i : Unit → SubProbability lens.ComplContent) (o : lens.ComplContent → SubProbability Unit) (h : a → SubProbability a) : h * lens.reduceSubProbability (f, i, o) = lens.reduceSubProbability (lens.liftSubProbability h * f, i, o)

Left Fubini identity. Pre-composing a reduced generator with h equals reducing the joint kernel pre-composed with the lift lens.liftSubProbability h.

theorem GaudisCrypt.Lens.reduceSubProbability_mul_right {a b : Type} (lens : Lens a b) (f : b → SubProbability b) (i : Unit → SubProbability lens.ComplContent) (o : lens.ComplContent → SubProbability Unit) (h : a → SubProbability a) : lens.reduceSubProbability (f, i, o) * h = lens.reduceSubProbability (f * lens.liftSubProbability h, i, o)

Right Fubini identity. Post-composing a reduced generator with h equals reducing the joint kernel post-composed with the lift lens.liftSubProbability h.

theorem GaudisCrypt.Lens.reduceSubProbability_ext {a b : Type} (lens : Lens a b) (K L : b → SubProbability b) (hKL : ∀ (i : Unit → SubProbability lens.ComplContent) (o : lens.ComplContent → SubProbability Unit), lens.reduceSubProbability (K, i, o) = lens.reduceSubProbability (L, i, o)) : K = L

Slice determination. A kernel K : b → SubProbability b is determined by all its reduced generators for a fixed lens: feeding a point input i = δ_β and an indicator weight o = [· = γ] recovers K on the slice splitSpace.invFun (·, β) restricted to complement-output γ. Ranging over all (β, γ) pins down K on every state. This is the one genuinely measure-theoretic ingredient (discreteMeasure.ext on singletons).

theorem GaudisCrypt.Lens.liftSubProbability_double_commutant {a b : Type} (lens : Lens a b) (W : Set (a → SubProbability a)) : lens.liftSubProbability '' W.centralizer.centralizer ⊆ (lens.liftSubProbability '' W).centralizer.centralizer

theorem GaudisCrypt.Lens.footprint_chain {a b c : Type} (lens1 : Lens b c) (lens2 : Lens a b) : (lens1.chain lens2).footprint = lens1.liftFootprint lens2.footprint

Footprint of a chained lens is the outer lens's lift of the inner footprint. Lens.chain lens1 lens2 threads through lens2 first and then lens1; the region it touches in the outer state is lens1.liftFootprint applied to lens2's footprint.

Only the ≤ direction is proved here (closure-monotonicity: the chain's generator range is the lens1-image of lens2's generator range, which sits inside the double-centralizer closure). The ≥ direction is open: it needs the corner/bicommutant-splitting structure of liftSubProbability, i.e. that lens1.liftSubProbability maps the double-centralizer closure of a generator set into the closure of its image.

theorem GaudisCrypt.Lens.footprint_fromLens {a b : Type} (l : Lens a b) : l.footprint.FromLens

Bicommutant scaffolding, lens-corner extraction, and Footprint.lens_pair

theorem GaudisCrypt.Footprint.ext {m : Type u_1} {x y : Footprint m} (h : x.updates = y.updates) : x = y

Two Footprints with the same updates are equal.

theorem GaudisCrypt.Footprint.ext_iff {m : Type u_1} {x y : Footprint m} : x = y ↔ x.updates = y.updates

@[simp]

theorem GaudisCrypt.Footprint.double_commutant_closed {m : Type u_1} (r : Footprint m) : r.updates.centralizer.centralizer = r.updates

Every Footprint is its own bicommutant (the double_commutant field, in Set form).

theorem GaudisCrypt.Footprint.sup_updates {m : Type u_1} (x y : Footprint m) : (x ⊔ y).updates = (x.updates ∪ y.updates).centralizer.centralizer

The updates of a join is the double centralizer of the union of the updates.

theorem GaudisCrypt.Footprint.from_union {m : Type u_1} (A B : Set (m → SubProbability m)) : «from» A ⊔ «from» B = «from» (A ∪ B)

theorem GaudisCrypt.Lens.liftSubProbability_injective {a s : Type} [Nonempty s] (lens : Lens a s) : Function.Injective lens.liftSubProbability

theorem GaudisCrypt.Lens.liftSubProbability_mul {a b : Type} (lens : Lens a b) (κ₁ κ₂ : a → SubProbability a) : lens.liftSubProbability (κ₁ * κ₂) = lens.liftSubProbability κ₁ * lens.liftSubProbability κ₂

lens.liftSubProbability is multiplicative, hence a monoid homomorphism on kernels. The lens laws (set_get, set_set) make the two localizations of a Kleisli composition agree.

@[implicit_reducible]

instance GaudisCrypt.instUniqueFootprintOfIsEmpty {s : Type u_1} [IsEmpty s] : Unique (Footprint s)

Equations

• GaudisCrypt.instUniqueFootprintOfIsEmpty = { default := ⊥, uniq := ⋯ }

theorem GaudisCrypt.Lens.liftFootprint_sup {a b : Type} (lens : Lens a b) (r₁ r₂ : Footprint a) : lens.liftFootprint (r₁ ⊔ r₂) = lens.liftFootprint r₁ ⊔ lens.liftFootprint r₂

theorem GaudisCrypt.Lens.footprint_updates {a s : Type} (lens : Lens a s) : lens.footprint.updates = (lens.liftSubProbability '' Set.univ).centralizer.centralizer

The bicommutant closure of the full set of lens-localized kernels is exactly lens.footprint. Since Lens.footprint is now generated by all localized kernels (Set.range lens.liftSubProbability = lens.liftSubProbability '' univ), this is definitional — what used to be the hard half of the lens-corner double-commutant theorem.

theorem GaudisCrypt.Lens.liftFootprint_updates {a b : Type} [Nonempty b] (lens : Lens a b) (range : Footprint a) : (lens.liftFootprint range).updates = lens.liftSubProbability '' range.updates

Lens.liftFootprint is exactly the lens-image of the footprint ([Nonempty b]). The ⊇ half is the generic X ⊆ CC X; the ⊆ half: Lens.liftFootprint lands in lens.footprint, every such element extracts as lens.liftSubProbability q, and (updateK being an injective hom) q inherits the commutation defining range.updates. Over a lens corner the bicommutant closure does not enlarge the image.

theorem GaudisCrypt.Lens.liftFootprint_chain {a b c : Type} (lens : Lens b c) (lens2 : Lens a b) (F : Footprint a) : (lens.chain lens2).liftFootprint F = lens.liftFootprint (lens2.liftFootprint F)

A chained lens's footprint-lift composes: lifting a base footprint through lens.chain lens2 is lifting through lens2 and then through lens.

theorem GaudisCrypt.Lens.compl_footprint {a s : Type} (l : Lens a s) : l.footprintᶜ = l.compl.footprint

A lens footprint's complement is its complement lens's footprint. The ≤ inclusion l.compl.footprint ≤ (l.footprint)ᶜ already exists (Lens.footprint_le_compl_of_disjoint l.compl l, used in footprint_equivariant); the reverse (l.footprint)ᶜ ≤ l.compl.footprint is the substantive half.

theorem GaudisCrypt.Footprint.disjoint_lens_footprint_inf {a s b : Type} (l1 : Lens a s) (l2 : Lens b s) [disjoint l1 l2] : l1.footprint ⊓ l2.footprint = ⊥

theorem GaudisCrypt.Footprint.lens_pair {a b m : Type} (x : Lens a m) (y : Lens b m) [disjoint x y] : (x.pair y).footprint = x.footprint ⊔ y.footprint

The footprint of a paired lens is the join of the components' footprints.

The ≥ direction is elementary: each component factors through the pair (pair_fst/pair_snd), so its footprint is a liftFootprint of a sub-⊤ footprint, hence ≤ the pair's own footprint.

The ≤ direction is the product/"corner"-structure theorem: lifting through the pair distributes over pair_footprint_fst_snd via Lens.liftFootprint_sup, and the two lifted corners are the component footprints by chain_footprint + pair_fst/pair_snd.

FromLens closure properties

Moved here from Language/Granularity.lean: these are general Footprint facts. They live below Footprint.lens_pair because Footprint.fromLens_sup needs it.

theorem GaudisCrypt.Footprint.fromLens_bot {s : Type} : ⊥.FromLens

theorem GaudisCrypt.Lens.disjoint_of_footprint_le_compl {a b s : Type} (x : Lens a s) (y : Lens b s) (h : x.footprint ≤ y.footprintᶜ) : disjoint x y

Converse of Lens.footprint_le_compl_of_disjoint: lenses whose footprints lie in each other's commutant have commuting setters. Both constant writes are Dirac kernels in their lens's footprint, so the commutant hypothesis makes them commute as kernels; evaluating at a state and stripping pure yields the plain set-commutation law.

theorem GaudisCrypt.Footprint.fromLens_sup {s : Type} {f g : Footprint s} (hf : f.FromLens) (hg : g.FromLens) (hd : f ≤ gᶜ) : (f ⊔ g).FromLens

Lens-derived footprints are closed under disjoint joins: pair the two lenses (the disjointness instance comes from Lens.disjoint_of_footprint_le_compl) and read off Footprint.lens_pair.

Lens.reduceFootprint (relocated from FV.lean)

noncomputable def GaudisCrypt.Lens.reduceFootprint {a b : Type} (lens : Lens a b) (range : Footprint b) : Footprint a

Equations

• lens.reduceFootprint range = GaudisCrypt.Footprint.from (lens.reduceSubProbability '' range.updates ×ˢ Set.univ ×ˢ Set.univ)

theorem GaudisCrypt.Lens.reduceFootprint_mono {a b : Type} (lens : Lens a b) {r r' : Footprint b} (h : r ≤ r') : lens.reduceFootprint r ≤ lens.reduceFootprint r'

Lens.reduceFootprint is monotone: a larger range gives a larger reduced range.

theorem GaudisCrypt.Lens.reduceFootprint_alt_def {a b : Type} (lens : Lens a b) (range : Footprint b) : lens.reduceFootprint range = Footprint.from {f : a → SubProbability a | ∀ g ∈ range.updates, lens.liftSubProbability f * g = g * lens.liftSubProbability f}.centralizer

theorem GaudisCrypt.Lens.reduceFootprint_sup {a b : Type} (lens : Lens a b) (r₁ r₂ : Footprint b) : lens.reduceFootprint (r₁ ⊔ r₂) = lens.reduceFootprint r₁ ⊔ lens.reduceFootprint r₂

theorem GaudisCrypt.Footprint.liftSubProbability_comm_reduce_compl {s c : Type} {L : Lens s c} {R : Footprint c} {f : s → SubProbability s} (hf : f ∈ (L.reduceFootprint R)ᶜ.updates) {k : c → SubProbability c} (hk : k ∈ R.updates) : L.liftSubProbability f * k = k * L.liftSubProbability f

The lift of an update commutes with every R-update, when the update commutes with the L-reduction of R (membership form: f ∈ (Lens.reduceFootprint L R)ᶜ.updates). The reduced generators reduceSubProbability L (k, i, o) of k ∈ R.updates lie in (Lens.reduceFootprint L R).updates, so hf makes them commute with f; the Fubini identities (Lens.reduceSubProbability_mul_left/_right) turn that into commutation of L.liftSubProbability f with k (via reduceSubProbability_ext).

@[simp]

theorem GaudisCrypt.Lens.reduceFootprint_compl_footprint {d s : Type} (L : Lens d s) : L.reduceFootprint L.footprintᶜ = ⊥

theorem GaudisCrypt.Footprint.reduceFootprint_updates {d s : Type} (L : Lens d s) (R : Footprint s) : (L.reduceFootprint R).updates = {f : d → SubProbability d | L.liftSubProbability f ∈ Rᶜ.updates}.centralizer

Lens.reduceFootprint in commutant form. (Lens.reduceFootprint L R).updates is the centralizer of the base kernels whose L-lift lands in Rᶜ (folding Lens.reduceFootprint_alt_def through Footprint.from).

theorem GaudisCrypt.Footprint.lift_reduceFootprint_eq {d s : Type} (L : Lens d s) (S : Footprint s) (hS : S ≤ L.footprint) : L.liftFootprint (L.reduceFootprint S) = S

theorem GaudisCrypt.Footprint.le_compl_comm {m : Type} (R S : Footprint m) : R ≤ Sᶜ ↔ S ≤ Rᶜ

Complement is order-reversing on Footprint (le/compl swap): R ≤ Sᶜ ↔ S ≤ Rᶜ. Both sides say every R-update commutes with every S-update, so the relation is symmetric in R, S.