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..66076c3e --- /dev/null +++ b/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 diff --git a/flake.nix b/flake.nix index 3f220b70..7c7c5702 100644 --- a/flake.nix +++ b/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`