mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat(lean): ProductSidon — injective product-space encoding from Sidon partition
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Xrttjg3619VRrMjxqUPUkL
This commit is contained in:
Claude
parent
475f6319ea
commit
817fbaca6c
1 changed files with 193 additions and 0 deletions
193
0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean
Normal file
193
0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue