Observational indistinguishability does not determine the touched getter

The converse of Footprint.indistinguishable_of_touched_getter_eq is false: two states can be indistinguishable through a footprint (no test of the footprint separates them by acceptance probability) while their touched_getter values differ.

The counterexample lives on Bool. Take the asymmetric lazy flip

qKer false = ½·δ_false + ½·δ_true, qKer true = ¼·δ_false + ¾·δ_true

and the footprint qCentralizer := (Footprint.from {qKer})ᶜ — everything commuting with qKer. Viewing kernels on Bool as substochastic 2×2 matrices, qKer is stochastic with distinct eigenvalues, so its commutant is the abelian algebra {α·I + β·qKer}:

• every member has both row sums equal to α + β, so every test mass is state-independent and false/true are indistinguishable (qCentralizer_indistinguishable) — formally, any h commuting with qKer satisfies m_f = ½·m_f + ½·m_t at false, forcing m_f = m_t;
• its only deterministic member is id (eq_id_of_comm: the swap would need ½ = ¼, the constants would need ½ ∈ {0, 1}), so the qCentralizerᶜ-orbits are trivial and the touched getter separates false from true (touched_getter_separates).

This is the same self-commutant abelian pathology behind LeastLens and the HasReset side-conditions — indeed qCentralizer has no reset anywhere (qCentralizer_not_hasReset), i.e. it is not a genuine memory region. For lens footprints the two notions agree.

noncomputable def GaudisCrypt.CounterExamples.flipPMF : PMF Bool

Fair coin on Bool.

Equations

• GaudisCrypt.CounterExamples.flipPMF = PMF.ofFintype (fun (x : Bool) => 2⁻¹) GaudisCrypt.CounterExamples.flipPMF._proof_2

noncomputable def GaudisCrypt.CounterExamples.biasPMF : PMF Bool

Biased coin: false ↦ ¼, true ↦ ¾.

Equations

• GaudisCrypt.CounterExamples.biasPMF = PMF.ofFintype (fun (b : Bool) => bif b then 3 * 4⁻¹ else 4⁻¹) GaudisCrypt.CounterExamples.biasPMF._proof_3

noncomputable def GaudisCrypt.CounterExamples.qKer : Bool → SubProbability Bool

The asymmetric lazy flip: fair from false, biased from true. A stochastic kernel with distinct "rows", whose commutant is abelian.

Equations

• GaudisCrypt.CounterExamples.qKer false = GaudisCrypt.toSubProbability GaudisCrypt.CounterExamples.flipPMF
• GaudisCrypt.CounterExamples.qKer true = GaudisCrypt.toSubProbability GaudisCrypt.CounterExamples.biasPMF

noncomputable def GaudisCrypt.CounterExamples.qCentralizer : Footprint Bool

The pathological footprint: everything commuting with qKer.

Equations

• GaudisCrypt.CounterExamples.qCentralizer = (GaudisCrypt.Footprint.from {GaudisCrypt.CounterExamples.qKer})ᶜ

Point evaluations of qKer

theorem GaudisCrypt.CounterExamples.qKer_false_apply (b : Bool) : ↑(qKer false) {b} = 2⁻¹

theorem GaudisCrypt.CounterExamples.qKer_true_apply_false : ↑(qKer true) {false} = 4⁻¹

theorem GaudisCrypt.CounterExamples.qKer_univ (σ : Bool) : ↑(qKer σ) Set.univ = 1

Generic evaluation helpers

Theorem A: no test separates false from true

theorem GaudisCrypt.CounterExamples.qCentralizer_indistinguishable : qCentralizer.indistinguishable false true

Any kernel commuting with qKer has state-independent total weight — evaluating the commutation equation at false gives m_f = ½·m_f + ½·m_t, hence m_f = m_t. So the two states of Bool are indistinguishable through qCentralizer.

Theorem B: the touched getter separates false from true

theorem GaudisCrypt.CounterExamples.eq_id_of_comm (f : Function.End Bool) (hcomm : qKer * diracKer f = diracKer f * qKer) : f = id

A deterministic kernel commuting with qKer is the identity: evaluating qKer (f false) = map f (qKer false) at the point false rules out the swap (¼ ≠ ½) and both constants (½ ∉ {0, 1} resp. ¼ ∉ {0, ½}).

theorem GaudisCrypt.CounterExamples.touched_getter_separates : qCentralizer.touched_getter.get false ≠ qCentralizer.touched_getter.get true

The qCentralizerᶜ-orbits are trivial (its only deterministic member is id), so the touched getter separates false from true.

The separation, and the tie-in with HasReset

theorem GaudisCrypt.CounterExamples.exists_indistinguishable_touched_getter_ne : ∃ (T : Footprint Bool) (σ : Bool) (σ' : Bool), T.indistinguishable σ σ' ∧ T.touched_getter.get σ ≠ T.touched_getter.get σ'

The two notions genuinely differ: indistinguishability through a footprint does not imply equal touched_getter — the converse of Footprint.indistinguishable_of_touched_getter_eq is false.

theorem GaudisCrypt.CounterExamples.qCentralizer_not_hasReset (σ : Bool) : ¬qCentralizer.HasReset σ

The pathological footprint is not a genuine memory region: it has no reset at any state (its only deterministic update is id, which cannot overwrite the — injective — touched content). The same abelian-bicommutant family that breaks HasReset breaks the tests-determine-glob converse.