Remark 13: Optimal Cheeger Constant

Statement

Picking a graph with Cheeger constant h(G) = 1 is optimal for distance preservation:

1. h(G) ≥ 1 is sufficient: By Lemma 3, d* ≥ d.
2. h(G) > 1 doesn't help further: Any nontrivial logical of the original code, supported only on vertex qubits, commutes with all deformed code checks since it acts trivially on edge qubits. Hence it is also a nontrivial logical of the deformed code, so d* ≤ d. Combined: d* = d when h(G) ≥ 1.
3. h(G) < 1 causes distance loss: d* ≥ h(G) · d < d.

Main Results

• liftToExtended : lifts a Pauli operator on V to V ⊕ E(G) with trivial edge action
• liftToExtended_weight : the lifted operator has the same weight
• liftToExtended_isLogical : lifting a pure-X original logical gives a deformed code logical
• deformed_distance_le_original : d* ≤ d (under existence of suitable pure-X logical)
• deformed_distance_eq : d* = d when h(G) ≥ 1
• cheeger_one_is_optimal : h(G) = 1 is the optimal threshold
• distance_loss_when_cheeger_lt_one : h(G) < 1 may cause distance loss

Lifting original operators to the extended system

def OptimalCheegerConstant.liftToExtended {V : Type u_1} (G : SimpleGraph V) (P : PauliOp V) : PauliOp (GaussFlux.ExtQubit G)

Lift a Pauli operator on V to V ⊕ E(G) with trivial (identity) action on edge qubits.

Equations

• OptimalCheegerConstant.liftToExtended G P = DeformedOperator.deformedOpExt G P 0

@[simp]

theorem OptimalCheegerConstant.liftToExtended_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (v : V) : (liftToExtended G P).xVec (Sum.inl v) = P.xVec v

@[simp]

theorem OptimalCheegerConstant.liftToExtended_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (e : ↑G.edgeSet) : (liftToExtended G P).xVec (Sum.inr e) = 0

@[simp]

theorem OptimalCheegerConstant.liftToExtended_zVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (v : V) : (liftToExtended G P).zVec (Sum.inl v) = P.zVec v

@[simp]

theorem OptimalCheegerConstant.liftToExtended_zVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (e : ↑G.edgeSet) : (liftToExtended G P).zVec (Sum.inr e) = 0

theorem OptimalCheegerConstant.liftToExtended_noX_on_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (e : ↑G.edgeSet) : (liftToExtended G P).xVec (Sum.inr e) = 0

theorem OptimalCheegerConstant.liftToExtended_noZ_on_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (e : ↑G.edgeSet) : (liftToExtended G P).zVec (Sum.inr e) = 0

theorem OptimalCheegerConstant.liftToExtended_weight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) : (liftToExtended G P).weight = P.weight

The lifted operator has the same weight as the original.

theorem OptimalCheegerConstant.restrictToV_liftToExtended {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) : SpaceDistance.restrictToV G (liftToExtended G P) = P

The restriction of a lifted operator back to V recovers the original.

theorem OptimalCheegerConstant.liftToExtended_mul {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp V) : liftToExtended G (P * Q) = liftToExtended G P * liftToExtended G Q

The lift preserves multiplication.

theorem OptimalCheegerConstant.liftToExtended_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : liftToExtended G 1 = 1

The lift sends identity to identity.

theorem OptimalCheegerConstant.liftToExtended_ne_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {P : PauliOp V} (hP : P ≠ 1) : liftToExtended G P ≠ 1

The lift is injective: it preserves non-identity.

Commutation of lifted operators with deformed code checks

theorem OptimalCheegerConstant.liftToExtended_comm_flux {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (_hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (P : PauliOp V) (p : C) : (liftToExtended G P).PauliCommute (DeformedCode.fluxChecks G cycles p)

The lift commutes with flux checks: flux is pure Z on edges, lift has no support on edges.

theorem OptimalCheegerConstant.liftToExtended_comm_deformedCheck {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (P : PauliOp V) (j : J) (hcomm_j : P.PauliCommute (checks j)) : (liftToExtended G P).PauliCommute (DeformedCode.deformedOriginalChecks G checks data j)

The lift commutes with deformed original checks when the original operator commutes with the original check.

theorem OptimalCheegerConstant.liftToExtended_symplecticInner_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (v : V) : (liftToExtended G P).symplecticInner (GaussFlux.gaussLawOp G v) = P.zVec v

⟨lift(P), A_v⟩ = P.zVec(v): the symplectic inner product with a gaussLaw check.

theorem OptimalCheegerConstant.liftToExtended_comm_gaussLaw_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (v : V) : (liftToExtended G P).PauliCommute (GaussFlux.gaussLawOp G v) ↔ P.zVec v = 0

The lift commutes with A_v iff P has no Z-support at v.

theorem OptimalCheegerConstant.liftToExtended_comm_gaussLaw_of_pureX {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (hpureX : P.zVec = 0) (v : V) : (liftToExtended G P).PauliCommute (GaussFlux.gaussLawOp G v)

A pure-X operator (zVec = 0) lifted to V ⊕ E commutes with all gaussLaw checks.

Pure-X logicals lift to deformed code centralizer

theorem OptimalCheegerConstant.liftToExtended_inCentralizer_of_pureX {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (P : PauliOp V) (hpureX : P.zVec = 0) (hcent : ∀ (j : J), P.PauliCommute (checks j)) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).inCentralizer (liftToExtended G P)

A pure-X operator in the centralizer of the original code lifts to the centralizer of the deformed code.

Point 1: h(G) ≥ 1 is sufficient for d* ≥ d

theorem OptimalCheegerConstant.sufficient_expansion_gives_dstar_ge_d {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (hconn : G.Connected) (hcard : 2 ≤ Fintype.card V) (hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ) (hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range) (hexp : DesiderataForGraphG.SufficientExpansion G) (hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV) (hDeformedHasLogicals : ∃ (P : PauliOp (GaussFlux.ExtQubit G)), (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P) : origCode.distance ≤ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance

Point 1: h(G) ≥ 1 is sufficient for d ≥ d.* Direct application of Lemma 3.

Point 2: d* ≤ d via lifting

theorem OptimalCheegerConstant.deformed_distance_le_weight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (L' : PauliOp (GaussFlux.ExtQubit G)) (hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L') : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance ≤ L'.weight

The deformed distance is at most the weight of any deformed code logical.

theorem OptimalCheegerConstant.liftToExtended_isLogical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (P : PauliOp V) (hlog : origCode.isLogicalOp P) (hpureX : P.zVec = 0) (hnotDeformedStab : liftToExtended G P ∉ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp (liftToExtended G P)

A pure-X logical P of the original code, when lifted, is a logical of the deformed code (given that the lift is not in the deformed stabilizer group).

theorem OptimalCheegerConstant.deformed_distance_le_original {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (P : PauliOp V) (hlog : origCode.isLogicalOp P) (hpureX : P.zVec = 0) (hweight : P.weight = origCode.distance) (hnotDeformedStab : liftToExtended G P ∉ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance ≤ origCode.distance

Point 2: d ≤ d.* If there exists a pure-X logical of minimum weight whose lift is not a deformed stabilizer, then d* ≤ d.

Point 2 combined with Point 1: d* = d when h(G) ≥ 1

theorem OptimalCheegerConstant.deformed_distance_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (hconn : G.Connected) (hcard : 2 ≤ Fintype.card V) (hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ) (hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range) (hexp : DesiderataForGraphG.SufficientExpansion G) (hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV) (hDeformedHasLogicals : ∃ (P : PauliOp (GaussFlux.ExtQubit G)), (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P) (P : PauliOp V) (hlog : origCode.isLogicalOp P) (hpureX : P.zVec = 0) (hweight : P.weight = origCode.distance) (hnotDeformedStab : liftToExtended G P ∉ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance = origCode.distance

d = d when h(G) ≥ 1* (combining Points 1 and 2).

Point 3: h(G) < 1 causes distance loss

theorem OptimalCheegerConstant.distance_loss_when_cheeger_lt_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (hconn : G.Connected) (hcard : 2 ≤ Fintype.card V) (hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ) (hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range) (hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV) (hDeformedHasLogicals : ∃ (P : PauliOp (GaussFlux.ExtQubit G)), (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P) (hCheeger_lt : QEC1.cheegerConstant G < 1) : QEC1.cheegerConstant G * ↑origCode.distance ≤ ↑(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance

Point 3: h(G) < 1 causes distance loss. The Lemma 3 bound gives d* ≥ h(G) · d, which is strictly less than d.

theorem OptimalCheegerConstant.cheeger_lt_one_bound_lt_d {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (origCode : StabilizerCode V) (hd : 0 < origCode.distance) (_hCheeger_pos : 0 < QEC1.cheegerConstant G) (hCheeger_lt : QEC1.cheegerConstant G < 1) : QEC1.cheegerConstant G * ↑origCode.distance < ↑origCode.distance

When h(G) < 1, the lower bound h(G) · d is strictly less than d (if d > 0 and h(G) > 0).

Optimality of h(G) = 1

theorem OptimalCheegerConstant.bound_saturates_at_cheeger_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (h : 1 ≤ QEC1.cheegerConstant G) (d : ℕ) : min (QEC1.cheegerConstant G) 1 * ↑d = ↑d

Increasing h(G) beyond 1 doesn't improve the Lemma 3 bound: min(h(G), 1) = 1.

@[simp]

theorem OptimalCheegerConstant.min_cheeger_one_eq_one_of_sufficient {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (h : DesiderataForGraphG.SufficientExpansion G) : min (QEC1.cheegerConstant G) 1 = 1

h(G) ≥ 1 implies min(h(G), 1) = 1.

theorem OptimalCheegerConstant.cheeger_gt_one_bound_eq_d {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (hconn : G.Connected) (hcard : 2 ≤ Fintype.card V) (hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ) (hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range) (hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV) (hDeformedHasLogicals : ∃ (P : PauliOp (GaussFlux.ExtQubit G)), (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P) (hCheeger : 1 < QEC1.cheegerConstant G) : origCode.distance ≤ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance

h(G) > 1 doesn't help further: the lower bound from Lemma 3 is still d.

Summary

theorem OptimalCheegerConstant.distance_trichotomy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (origCode : StabilizerCode V) (hd : 0 < origCode.distance) (hCheeger_pos : 0 < QEC1.cheegerConstant G) : (1 ≤ QEC1.cheegerConstant G → min (QEC1.cheegerConstant G) 1 * ↑origCode.distance = ↑origCode.distance) ∧ (QEC1.cheegerConstant G < 1 → min (QEC1.cheegerConstant G) 1 * ↑origCode.distance < ↑origCode.distance)

The distance bound trichotomy:

• h(G) ≥ 1 → the bound gives d (saturates)
• h(G) < 1 → the bound gives h(G)·d < d (distance loss)