proof

P17 Labels ≠ bearer map

Lean spine source

Declarations: P17_same_value_words_not_same_bearer_map

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P17_same_value_words_not_same_bearer_map :
    ∃ p q : ValueProfile 2 3,
      sameValueLabels p q ∧ ¬ sameBearerMap p q :=
  ⟨valueProfile0, valueProfile1, same_value_labels_profiles, different_bearer_map_profiles⟩

/-- Tradeoff geometry: marginals and bundle interaction curvature (ch19 Hessian proxy). -/