Merge branch 'claude/beautiful-mayer-2zczgq' of https://github.com/allaunthefox/Research-Stack

0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean

@@ -0,0 +1,191 @@
+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. `product_sidon_injective` extends this to *cross*-differences between
+  two sets.
+- `sidon_partition_implies_product_sidon`: 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 product_sidon_injective
+    (α : X → ℤ) (β : Y → ℤ)
+    (hα : Function.Injective α) (hβ : Function.Injective β)
+    (hdisj : CrossDiffDisjoint α β) :
+    IsProductSidon α β := by
+  intro ⟨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 is_product_sidon_iff_cross_diff_disjoint
+    (α : 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 congrArg α (Prod.ext_iff.mp hpair).1
+  · exact product_sidon_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 sidon_partition_implies_product_sidon
+    (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
+  -- 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 is_product_sidon_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

flake.nix

@@ -188,81 +188,6 @@
         mkdir -p -m 1777 $out/tmp
       '';
 
-      # ── rs-surface binary ───────────────────────────────────────────────────
-      # Rust port of 4-Infrastructure/infra/embedded_surface/server.py.
-      # Build the binary hermetically via rustPlatform.buildRustPackage.
-      #
-      # cargoHash: run `nix build .#rs-surface 2>&1 | grep "got:"` to get the
-      # real hash after any Cargo.lock change, then replace lib.fakeHash below.
-      rsSurface = pkgs.rustPlatform.buildRustPackage {
-        pname   = "rs-surface";
-        version = "0.1.0";
-
-        src = pkgs.lib.cleanSource ./4-Infrastructure/infra/embedded_surface/rs-surface;
-
-        cargoLock.lockFile = ./4-Infrastructure/infra/embedded_surface/rs-surface/Cargo.lock;
-
-        nativeBuildInputs = [ pkgs.pkg-config ];
-        buildInputs       = [ pkgs.openssl ];
-
-        meta = {
-          description = "Embedded node surface daemon (Rust)";
-          license     = pkgs.lib.licenses.mit;
-          mainProgram = "rs-surface";
-        };
-      };
-
-      # ── Minimal OCI image for the embedded node surface ────────────────────
-      # Built entirely from the Nix store — no Dockerfile, no Alpine, no musl.
-      # The closure contains only the binary + its glibc runtime deps.
-      #
-      # Build:  nix build .#rs-surface-image
-      # Load:   docker load < result
-      # Run:    docker run --rm -p 8080:8080 -v /etc/rs-surface:/etc/rs-surface rs-surface:latest
-      rsSurfaceImage = pkgs.dockerTools.buildLayeredImage {
-        name = "rs-surface";
-        tag  = "latest";
-
-        contents = [
-          rsSurface
-          pkgs.cacert          # TLS roots (for any outbound HTTPS)
-          pkgs.coreutils       # minimal shell utilities for healthcheck
-        ];
-
-        # /etc/rs-surface/node.json is volume-mounted at runtime; create the
-        # directory so the mount point exists in the image.
-        extraCommands = ''
-          mkdir -p etc/rs-surface var/lib/rs-surface mnt/topological-storage
-        '';
-
-        config = {
-          Entrypoint = [ "${rsSurface}/bin/rs-surface" ];
-          Env = [
-            "RS_SURFACE_PROFILE=/etc/rs-surface/node.json"
-            "RS_SURFACE_STATE=/var/lib/rs-surface"
-            "RS_SURFACE_MOUNT=/mnt/topological-storage"
-            "RS_SURFACE_HOST=0.0.0.0"
-            "RS_SURFACE_PORT=8080"
-            "SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"
-          ];
-          ExposedPorts = { "8080/tcp" = {}; };
-          Healthcheck = {
-            Test        = [ "CMD" "${pkgs.coreutils}/bin/sh" "-c"
-              "wget -qO- http://127.0.0.1:8080/health || exit 1" ];
-            Interval    = 10000000000;   # 10 s in nanoseconds
-            Timeout     = 3000000000;    # 3 s
-            StartPeriod = 3000000000;    # 3 s
-            Retries     = 3;
-          };
-          Labels = {
-            "org.opencontainers.image.description" = "rs-surface embedded node daemon";
-            "org.opencontainers.image.source"      = "4-Infrastructure/infra/embedded_surface/rs-surface";
-          };
-        };
-
-        maxLayers = 10;
-      };
-
     in rec {
       packages.${system} = {
 
@@ -303,9 +228,6 @@
           maxLayers = 120;
         };
 
-        # rs-surface binary and OCI image
-        rs-surface       = rsSurface;
-        rs-surface-image = rsSurfaceImage;
       };
 
       # Convenience alias: `nix build .#devcontainer`