mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
4490dc28a7
- Move canonical FixedPoint to Core/SilverSight/FixedPoint.lean - Add SilverSightRRC library: RRC logogram gates, receipt bridge, AVM ISA - Add AVMIsa.Emit as the sole top-level JSON output boundary - Add rrc-emit-fixture executable and Python I/O shims - Update AGENTS.md, glossary, project map, and build baseline Build: 2981 jobs, 0 errors (lake build)
112 lines
5.9 KiB
Text
112 lines
5.9 KiB
Text
/-
|
||
SieveLemmas.lean -- Number-theoretic lemmas for coprime sieve observers
|
||
|
||
This module formalizes the CRT reconstruction principle referenced in
|
||
ImaginarySemanticTime.lean: two observers with coprime native sieve moduli
|
||
hold independent, complementary shadows of the same underlying manifold
|
||
coordinate. Neither observer can recover the other's view without a CRT
|
||
exchange, but together they reconstruct the coordinate modulo the product.
|
||
|
||
Key lemma: depth_token_coprime_intersect — the observations of two coprime
|
||
sieves intersect in exactly one residue class modulo ℓ₁·ℓ₂, which is the
|
||
original semantic coordinate's residue class.
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.GCD.BigOperators
|
||
import Mathlib.Data.ZMod.Basic
|
||
|
||
namespace SilverSight.SieveLemmas
|
||
|
||
open Nat
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §1 Sieve observations and coprimality
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- A sieve modulus is a positive natural number used as a native resolution.
|
||
We bundle the positivity proof so that modular operations are well-behaved. -/
|
||
structure SieveModulus where
|
||
val : Nat
|
||
pos : val > 0
|
||
deriving Repr
|
||
|
||
/-- Observation of a semantic coordinate `x` through a sieve modulus `ℓ`. -/
|
||
def observe (ℓ : SieveModulus) (x : Nat) : Nat := x % ℓ.val
|
||
|
||
/-- Two sieve moduli are coprime observers when their values are coprime. -/
|
||
def CoprimeObservers (ℓ1 ℓ2 : SieveModulus) : Prop :=
|
||
Coprime ℓ1.val ℓ2.val
|
||
|
||
instance {ℓ1 ℓ2 : SieveModulus} : Decidable (CoprimeObservers ℓ1 ℓ2) := by
|
||
unfold CoprimeObservers; infer_instance
|
||
|
||
/-- An observation is always smaller than its sieve modulus. -/
|
||
lemma observe_lt (ℓ : SieveModulus) (x : Nat) : observe ℓ x < ℓ.val := by
|
||
simp only [observe]
|
||
apply mod_lt
|
||
exact ℓ.pos
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §2 CRT reconstruction
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- Reconstruct the unique residue modulo ℓ₁·ℓ₂ that projects to `r1` and `r2`.
|
||
Returns 0 if either modulus is invalid (defensive, since SieveModulus is positive). -/
|
||
def crtReconstruct (ℓ1 ℓ2 : SieveModulus) (r1 r2 : Nat) (hc : CoprimeObservers ℓ1 ℓ2) : Nat :=
|
||
(chineseRemainder hc r1 r2).val
|
||
|
||
/-- The CRT reconstruction is correct modulo the first observer's modulus. -/
|
||
theorem crtReconstruct_mod_ℓ1 (ℓ1 ℓ2 : SieveModulus) (r1 r2 : Nat)
|
||
(hc : CoprimeObservers ℓ1 ℓ2) :
|
||
crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ1.val = r1 % ℓ1.val := by
|
||
simp [crtReconstruct]
|
||
exact (chineseRemainder hc r1 r2).property.left
|
||
|
||
/-- The CRT reconstruction is correct modulo the second observer's modulus. -/
|
||
theorem crtReconstruct_mod_ℓ2 (ℓ1 ℓ2 : SieveModulus) (r1 r2 : Nat)
|
||
(hc : CoprimeObservers ℓ1 ℓ2) :
|
||
crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ2.val = r2 % ℓ2.val := by
|
||
simp [crtReconstruct]
|
||
exact (chineseRemainder hc r1 r2).property.right
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §3 The coprime-intersection theorem (depth-token view)
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- The observations of two coprime sieve observers uniquely determine the
|
||
semantic coordinate modulo ℓ₁·ℓ₂. This is the "depth-token coprime
|
||
intersection": two independent sieve depths coincide at exactly one
|
||
residue class of the product modulus. -/
|
||
theorem depth_token_coprime_intersect
|
||
(ℓ1 ℓ2 : SieveModulus) (x : Nat) (hc : CoprimeObservers ℓ1 ℓ2) :
|
||
let r1 := observe ℓ1 x
|
||
let r2 := observe ℓ2 x
|
||
crtReconstruct ℓ1 ℓ2 r1 r2 hc % (ℓ1.val * ℓ2.val) = x % (ℓ1.val * ℓ2.val) := by
|
||
intro r1 r2
|
||
have h1 : crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ1.val = x % ℓ1.val := by
|
||
rw [crtReconstruct_mod_ℓ1 ℓ1 ℓ2 r1 r2 hc]
|
||
simp [observe, r1]
|
||
have h2 : crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ2.val = x % ℓ2.val := by
|
||
rw [crtReconstruct_mod_ℓ2 ℓ1 ℓ2 r1 r2 hc]
|
||
simp [observe, r2]
|
||
exact (modEq_and_modEq_iff_modEq_mul hc).mp ⟨h1, h2⟩
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §4 Witness
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- Human (ℓ=7) and dolphin (ℓ=11) reconstruct 61 mod 77. -/
|
||
def humanℓ : SieveModulus := ⟨7, by decide⟩
|
||
def dolphinℓ : SieveModulus := ⟨11, by decide⟩
|
||
def shared : Nat := 61
|
||
|
||
def humanShadow : Nat := observe humanℓ shared
|
||
def dolphinShadow : Nat := observe dolphinℓ shared
|
||
def reconciled : Nat :=
|
||
crtReconstruct humanℓ dolphinℓ humanShadow dolphinShadow (by decide)
|
||
|
||
#eval humanShadow -- 5
|
||
#eval dolphinShadow -- 6
|
||
#eval! reconciled -- 61
|
||
|
||
end SilverSight.SieveLemmas
|