DetermFootprint — LEGACY deterministic range theory (quarantined)

Deprecated / quarantined. The deterministic (Function.End-based) lens-range theory, superseded by Footprint (sub-probability kernels — countability-free, self-range holds). Retained only for CounterExamples and not-yet-migrated consumers. New code: use Footprint.

structure DetermFootprint (m : Type u_1) : Type u_1

• updates : Set (Function.End m)
• id : _root_.id ∈ self.updates
• comp {f g : Function.End m} : f ∈ self.updates → g ∈ self.updates → f ∘ g ∈ self.updates
• double_commutant : (Submonoid.centralizer (Submonoid.centralizer self.updates).carrier).carrier = self.updates

@[implicit_reducible]

instance instComplDetermFootprint {m : Type u_1} : Compl (DetermFootprint m)

Equations

• instComplDetermFootprint = { compl := fun (range : DetermFootprint m) => { updates := (Submonoid.centralizer range.updates).carrier, id := ⋯, comp := ⋯, double_commutant := ⋯ } }

def GaudisCrypt.Lens.range {a : Type u_1} {m : Type u_2} (lens : Lens a m) : DetermFootprint m

Equations

• lens.range = { updates := lens.liftFunction '' ⊤, id := ⋯, comp := ⋯, double_commutant := ⋯ }

theorem DetermFootprint.complement_range {a : Type u_1} {m : Type u_2} (lens : GaudisCrypt.Lens a m) : lens.compl.range = lens.rangeᶜ

def DetermFootprint.from {m : Type u_1} (generators : Set (Function.End m)) : DetermFootprint m

Equations

• DetermFootprint.from generators = { updates := ↑(Submonoid.centralizer (Submonoid.centralizer generators).carrier), id := ⋯, comp := ⋯, double_commutant := ⋯ }

@[implicit_reducible]

instance instPartialOrderDetermFootprint {m : Type u_1} : PartialOrder (DetermFootprint m)

Equations

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

@[implicit_reducible]

instance instLatticeDetermFootprint {m : Type u_1} : Lattice (DetermFootprint m)

Equations

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

@[implicit_reducible]

instance instBoundedOrderDetermFootprint {m : Type u_1} : BoundedOrder (DetermFootprint m)

Equations

• instBoundedOrderDetermFootprint = { top := { updates := ⊤, id := ⋯, comp := ⋯, double_commutant := ⋯ }, le_top := ⋯, bot := DetermFootprint.from ∅, bot_le := ⋯ }

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

theorem Lens.range_le_compl_of_disjoint {a b m : Type} (v : GaudisCrypt.Lens a m) (L : GaudisCrypt.Lens b m) [hd : GaudisCrypt.disjoint v L] : v.range ≤ L.compl.range

Disjoint lenses have ranges contained in each other's complements: if disjoint v L, then every v-update lives in L.compl.range.

@[implicit_reducible]

instance instCompleteSemilatticeSupDetermFootprint {m : Type u_1} : CompleteSemilatticeSup (DetermFootprint m)

Equations

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

@[implicit_reducible]

instance instCompleteSemilatticeInfDetermFootprint {m : Type u_1} : CompleteSemilatticeInf (DetermFootprint m)

Equations

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

@[implicit_reducible]

instance instCompleteLatticeDetermFootprint {m : Type u_1} : CompleteLattice (DetermFootprint m)

Equations

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

theorem Lens.range_defines_preorder {m : Type u_1} {a b : Type u_2} [Nonempty m] (x : GaudisCrypt.Lens a m) (y : GaudisCrypt.Lens b m) : x.range ≤ y.range ↔ GaudisCrypt.LensIn.mk' x ≤ GaudisCrypt.LensIn.mk' y

noncomputable def LensIn.antisymmOrderEmb {m : Type u_1} [Nonempty m] : (Antisymmetrization (GaudisCrypt.LensIn m) fun (x1 x2 : GaudisCrypt.LensIn m) => x1 ≤ x2) ↪o DetermFootprint m

Equations

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

Orbits and the global getter

def DetermFootprint.orbit_setoid {m : Type u_1} (R : DetermFootprint m) : Setoid m

The R-orbit equivalence on m: s ~ s' iff one is reachable from the other via R-updates (the equivalence closure of the directed orbit relation, since R is a monoid not a group).

Equations

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

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

The "global getter" of a DetermFootprint: the quotient projection onto orbit-classes.

Reading: two states give the same getter value iff they are in the same R-orbit.

For a lens-derived range R = l.range, two states are in the same R-orbit iff they differ only in l's content — so this getter encodes the complement of l.

Convention: glob A is typically "what A touches", i.e. the commutant's orbits, so one writes glob A := A.range.commutant.global_getter (commutant = Rᶜ). Equivalently glob A := A.rangeᶜ.global_getter.

Equations

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

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

The "touched" getter: the same construction applied to the commutant. For a lens-derived range R = l.range, this is isomorphic to l.toGetter.

Equations

• R.touched_getter = Rᶜ.global_getter