proof

P14 Bundle factorization

Lean spine source

Declarations: P14_factorization_implies_equivalent_errors

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P14_factorization_implies_equivalent_errors
    {f : Error → Action} {c : Error → Bundle}
    (h : FactorsThrough f c)
    {e₁ e₂ : Error}
    (heq : c e₁ = c e₂) :
    f e₁ = f e₂ := by
  obtain ⟨d, hd⟩ := h
  rw [hd]
  simp [Function.comp, heq]

/-- A toy sample predicate: there are enough observations for a `K`-dimensional
    LHV readout. This deliberately abstracts away constants and horizons. -/