From 2942a15e210dc4c6c79f42b00f1cc18d2190ccaf Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 06:41:55 +0000 Subject: [PATCH] =?UTF-8?q?feat(lean):=20ProductSidon=20=E2=80=94=20inject?= =?UTF-8?q?ive=20product-space=20encoding=20from=20Sidon=20partition?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Formalizes the core equation extracted from atproto's "no instances" principle: α(x₁) + β(y₁) = α(x₂) + β(y₂) → x₁ = x₂ ∧ y₁ = y₂ Key additions (0 sorry): - IsProductSidon: injectivity of joint encoding f(x,y) = α(x) + β(y) - CrossDiffDisjoint: (Δ image α) ∩ (Δ image β) = {0} - productSidon_injective: CrossDiffDisjoint → IsProductSidon - isProductSidon_iff_crossDiffDisjoint: equivalence (given injective encodings) - sidonPartition_implies_productSidon: Sidon set partition → ProductSidon pair - atmosphere_sidon_principle: equal observables → same host/app decomposition Extends sidon_diff_injective (E8Sidon §8) from intra-set to cross-set differences. Co-Authored-By: Claude Sonnet 4.6 Claude-Session: https://claude.ai/code/session_01Xrttjg3619VRrMjxqUPUkL --- .../Semantics/Semantics/ProductSidon.lean | 193 ++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean diff --git a/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean new file mode 100644 index 00000000..da0c283d --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean @@ -0,0 +1,193 @@ +import Mathlib.Data.Int.Defs +import Mathlib.Data.Finset.Basic +import Semantics.E8Sidon + +/-! # Product Sidon Injectivity + +## The Equation + +Stripping away all social-network semantics from the atproto architecture, +the central claim reduces to one equation: + + **If `α(x₁) + β(y₁) = α(x₂) + β(y₂)` then `x₁ = x₂` and `y₁ = y₂`.** + +This is exactly the injectivity condition on the joint encoding `f(x,y) = α(x) + β(y)`. + +## Sidon Connection + +The necessary and sufficient condition for this injectivity (given `α`, `β` injective) +is that no nonzero difference from `image(α)` equals any nonzero difference from `image(β)`: + + **(Δ image(α)) ∩ (Δ image(β)) = {0}** + +This is the *cross-difference disjointness* condition. It is implied by +`image(α) ∪ image(β)` being a Sidon set — a bridge to the E₈ Sidon framework +in `Semantics.E8Sidon`. + +## Interpretation + +In atproto terms: +- `α` encodes hosting providers (H) +- `β` encodes app projections (A) +- The encoding `f(H, A) = α(H) + β(A)` is injective iff cross-differences don't collide + +If the joint (H, A)-encoding is product-Sidon, then two observable states being +equal forces the underlying host/app decompositions to be equal. This is the +"no instances" property: data identity is primary, projections cannot masquerade +as each other. The Sidon uniqueness condition *is* the decentralization invariant. + +## Relation to existing infrastructure + +- `sidon_diff_injective` (E8Sidon §8): differences within a *single* Sidon set are + injective. `productSidon_injective` extends this to *cross*-differences between + two sets. +- `sidonPartition_implies_productSidon`: if a Sidon set is partitioned into two + disjoint blocks used as encoding ranges, the cross-difference condition holds + automatically. +-/ + +namespace Semantics.ProductSidon + +open Semantics.E8Sidon + +variable {X Y : Type*} + +/-! ## Core definitions -/ + +/-- A pair of encodings `(α, β)` is *product-Sidon* if the joint encoding + `f(x, y) = α(x) + β(y)` is injective as a function on `X × Y`. -/ +def IsProductSidon (α : X → ℤ) (β : Y → ℤ) : Prop := + Function.Injective (fun p : X × Y => α p.1 + β p.2) + +/-- Cross-difference disjointness: any α-difference that equals a β-difference + must be zero. Equivalently, no nonzero α-difference equals any β-difference. -/ +def CrossDiffDisjoint (α : X → ℤ) (β : Y → ℤ) : Prop := + ∀ x₁ x₂ : X, ∀ y₁ y₂ : Y, + α x₁ - α x₂ = β y₂ - β y₁ → α x₁ = α x₂ + +/-! ## The main theorem -/ + +/-- **Product Sidon Injectivity**: given injective encodings `α`, `β` with + cross-difference disjoint images, the joint encoding `f(x,y) = α(x) + β(y)` + is injective. + + This is the key equation: `α(x₁) + β(y₁) = α(x₂) + β(y₂)` implies + `x₁ = x₂` and `y₁ = y₂`. -/ +theorem productSidon_injective + (α : X → ℤ) (β : Y → ℤ) + (hα : Function.Injective α) (hβ : Function.Injective β) + (hdisj : CrossDiffDisjoint α β) : + IsProductSidon α β := by + intro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩ heq + have heq' : α x₁ + β y₁ = α x₂ + β y₂ := heq + have hdiff : α x₁ - α x₂ = β y₂ - β y₁ := by linarith + have hαeq : α x₁ = α x₂ := hdisj x₁ x₂ y₁ y₂ hdiff + have hβeq : β y₁ = β y₂ := by linarith + exact Prod.ext (hα hαeq) (hβ hβeq) + +/-- The equivalence: `IsProductSidon` iff `CrossDiffDisjoint` + (given injective encodings). -/ +theorem isProductSidon_iff_crossDiffDisjoint + (α : X → ℤ) (β : Y → ℤ) + (hα : Function.Injective α) (hβ : Function.Injective β) : + IsProductSidon α β ↔ CrossDiffDisjoint α β := by + constructor + · intro hinj x₁ x₂ y₁ y₂ hdiff + have heq : α x₁ + β y₁ = α x₂ + β y₂ := by linarith + have hpair : (x₁, y₁) = (x₂, y₂) := hinj heq + exact congr_arg α (Prod.ext_iff.mp hpair).1 + · exact productSidon_injective α β hα hβ + +/-! ## Bridge from Sidon sets -/ + +/-- **Sidon Partition → Product Sidon**: if a Sidon set `S` is split into + two disjoint parts `A` and `B`, and `α` maps into `A` while `β` maps into `B`, + then `(α, β)` is product-Sidon. + + *Proof*: Sidon says `α(x₁) + β(y₁) = α(x₂) + β(y₂)` implies + `{α(x₁), β(y₁)} = {α(x₂), β(y₂)}`. Since `A ∩ B = ∅`, we cannot have + `α(x₁) = β(y₂)` (different parts), so `α(x₁) = α(x₂)` and `β(y₁) = β(y₂)`. -/ +theorem sidonPartition_implies_productSidon + (S A B : Finset ℤ) + (hS : IsSidonSet S) + (hAB_union : A ∪ B = S) + (hAB_disj : Disjoint A B) + (α : X → ℤ) (β : Y → ℤ) + (hα_range : ∀ x, α x ∈ A) + (hβ_range : ∀ y, β y ∈ B) + (hα_inj : Function.Injective α) + (hβ_inj : Function.Injective β) : + IsProductSidon α β := by + intro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩ heq + have heq' : α x₁ + β y₁ = α x₂ + β y₂ := heq + -- All four values lie in S + have hαx₁S : α x₁ ∈ S := hAB_union ▸ Finset.mem_union_left B (hα_range x₁) + have hβy₁S : β y₁ ∈ S := hAB_union ▸ Finset.mem_union_right A (hβ_range y₁) + have hαx₂S : α x₂ ∈ S := hAB_union ▸ Finset.mem_union_left B (hα_range x₂) + have hβy₂S : β y₂ ∈ S := hAB_union ▸ Finset.mem_union_right A (hβ_range y₂) + -- Apply the Sidon property + rcases hS (α x₁) hαx₁S (β y₁) hβy₁S (α x₂) hαx₂S (β y₂) hβy₂S heq' with + (⟨h1, h2⟩ | ⟨h1, h2⟩) + · -- Case 1: α x₁ = α x₂ ∧ β y₁ = β y₂ → done by injectivity + exact Prod.ext (hα_inj h1) (hβ_inj h2) + · -- Case 2: α x₁ = β y₂ → contradicts A ∩ B = ∅ + exfalso + have hαx₁_in_B : α x₁ ∈ B := by rw [h1]; exact hβ_range y₂ + exact Finset.disjoint_left.mp hAB_disj (hα_range x₁) hαx₁_in_B + +/-! ## The Atmosphere Sidon Principle -/ + +/-- **Atmosphere Sidon Principle**: if the (host, app) joint encoding is + product-Sidon, then any two equal observables arose from the same + host/app decomposition. + + `β h₁ + γ a₁ = β h₂ + γ a₂ → h₁ = h₂ ∧ a₁ = a₂` + + This is the formal content of "there are no instances" in atproto: + data identity `D` is primary; if two projection paths + `π_{A₁} ∘ σ_{H₁}(D)` and `π_{A₂} ∘ σ_{H₂}(D)` yield the same + observable state, the paths themselves must be equal. + The Sidon uniqueness condition *is* the decentralization invariant. -/ +theorem atmosphere_sidon_principle + {Host App : Type*} + (β : Host → ℤ) (γ : App → ℤ) + (hProductSidon : IsProductSidon β γ) + {h₁ h₂ : Host} {a₁ a₂ : App} + (hobs : β h₁ + γ a₁ = β h₂ + γ a₂) : + h₁ = h₂ ∧ a₁ = a₂ := + Prod.ext_iff.mp (hProductSidon hobs) + +/-- **Corollary**: equal observables under product-Sidon encoding imply + the first coordinates (hosts) are equal. -/ +theorem atmosphere_host_eq + {Host App : Type*} + (β : Host → ℤ) (γ : App → ℤ) + (hProductSidon : IsProductSidon β γ) + {h₁ h₂ : Host} {a₁ a₂ : App} + (hobs : β h₁ + γ a₁ = β h₂ + γ a₂) : + h₁ = h₂ := + (atmosphere_sidon_principle β γ hProductSidon hobs).1 + +/-- **Corollary**: equal observables under product-Sidon encoding imply + the second coordinates (apps) are equal. -/ +theorem atmosphere_app_eq + {Host App : Type*} + (β : Host → ℤ) (γ : App → ℤ) + (hProductSidon : IsProductSidon β γ) + {h₁ h₂ : Host} {a₁ a₂ : App} + (hobs : β h₁ + γ a₁ = β h₂ + γ a₂) : + a₁ = a₂ := + (atmosphere_sidon_principle β γ hProductSidon hobs).2 + +/-! ## Symmetric version -/ + +/-- Product-Sidon is symmetric: if `(α, β)` is product-Sidon, then so is `(β, α)`. + (Swapping host and app roles doesn't break injectivity.) -/ +theorem isProductSidon_symm (α : X → ℤ) (β : Y → ℤ) + (h : IsProductSidon α β) : IsProductSidon β α := by + intro ⟨y₁, x₁⟩ ⟨y₂, x₂⟩ heq + have heq' : α x₁ + β y₁ = α x₂ + β y₂ := by linarith + have hpair : (x₁, y₁) = (x₂, y₂) := h heq' + exact Prod.ext (Prod.ext_iff.mp hpair).2 (Prod.ext_iff.mp hpair).1 + +end Semantics.ProductSidon