mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-13 07:40:33 +00:00
docs: fix documentation gaps + add pure math description
Fixed 5 undocumented Lean files: - PVGS_DQ_Bridge/section5_quantum_sensing.lean — quantum sensing docs - PVGS_DQ_Bridge/section2_hermite_sieve.lean — Hermite polynomial docs - SilverSight/RRC/ReceiptDensity.lean — receipt density scoring docs - SilverSight/PIST/SpectralWitness.lean — spectral witness docs - CoreFormalism/FixedPoint.lean — stub redirect docs Added docs/PURE_MATH_DESCRIPTION.md: - Pure mathematical description of each module (no code) - Why each module exists (problem/insight) - What a graph calculator would need to implement each - 10 modules covered: SidonSets, BraidEigensolid, BraidSpherionBridge, HachimojiLUT, ChentsovFinite, DynamicCanal, Schema, WireFormat, Receipt, Bind
This commit is contained in:
parent
1a26de076d
commit
f7858914b7
6 changed files with 687 additions and 0 deletions
556
docs/PURE_MATH_DESCRIPTION.md
Normal file
556
docs/PURE_MATH_DESCRIPTION.md
Normal file
|
|
@ -0,0 +1,556 @@
|
|||
# SilverSight Modules — Pure Mathematical Description
|
||||
|
||||
This document describes each SilverSight module in pure mathematical
|
||||
terms. No code, no implementation details — only the mathematical
|
||||
structures, theorems, and insights each module embodies.
|
||||
|
||||
---
|
||||
|
||||
## SidonSets
|
||||
|
||||
### What it does
|
||||
|
||||
Defines the **Sidon property** for finite sets of integers and proves
|
||||
extremal bounds on Sidon subsets of $\{1, \ldots, N\}$.
|
||||
|
||||
A finite set $A \subset \mathbb{Z}$ is **Sidon** (or a $B_2$-set) if
|
||||
every pairwise sum is unique up to reordering:
|
||||
|
||||
$$\forall\, a, b, c, d \in A:\quad a + b = c + d \implies \{a,b\} = \{c,d\}$$
|
||||
|
||||
The **modular variant** $A$ is Sidon modulo $M$ when:
|
||||
|
||||
$$M \mid (a+b) - (c+d) \implies \{a,b\} = \{c,d\}$$
|
||||
|
||||
The **extremal function** $h(N) = \max\{|A| : A \subseteq \{1,\ldots,N\}
|
||||
\text{ is Sidon}\}$ is shown to exist and be unique for every $N$.
|
||||
|
||||
Two upper bounds are proved:
|
||||
|
||||
1. **Difference-counting bound:** $h(N) \leq \sqrt{2N} + 1$, obtained by
|
||||
counting the $\binom{|A|}{2}$ distinct positive differences $a - b$
|
||||
and noting they all lie in $\{1, \ldots, N-1\}$.
|
||||
|
||||
2. **Lindström's bound** (via the Johnson/Cauchy-Schwarz method):
|
||||
$h(N) \leq \sqrt{N} + \sqrt[4]{N} + 2$ for $N \geq 16$.
|
||||
This is proved by considering $m$ shifted copies $A, A+1, \ldots,
|
||||
A+(m-1)$ of a Sidon set, applying the incidence inequality
|
||||
$(\sum_i |S_i|)^2 \leq |U| \cdot \sum_{i,j} |S_i \cap S_j|$,
|
||||
and using the Sidon property to bound off-diagonal intersections
|
||||
by 1.
|
||||
|
||||
The **Singer construction** produces, for every prime $p$, a Sidon set
|
||||
modulo $p^2 + p + 1$ of cardinality $p + 1$. The construction uses:
|
||||
|
||||
- The degree-3 Galois extension $\mathbb{F}_{p^3} / \mathbb{F}_p$.
|
||||
- The trace kernel $V = \ker(\text{Tr}_{\mathbb{F}_{p^3}/\mathbb{F}_p})$,
|
||||
a 2-dimensional $\mathbb{F}_p$-subspace.
|
||||
- The quotient group $\mathbb{F}_{p^3}^\times / \mathbb{F}_p^\times$,
|
||||
which is cyclic of order $p^2 + p + 1$.
|
||||
- A geometric lemma: for $\alpha \notin \mathbb{F}_p$, the intersection
|
||||
$V \cap \alpha^{-1}V$ has dimension exactly 1. This is the core
|
||||
geometric fact that forces the Sidon property in the quotient.
|
||||
|
||||
### Why it does it
|
||||
|
||||
Sidon sets are the address-space backbone of the compressor. The 8
|
||||
strands of the BraidStorm use Sidon labels $\{1, 2, 4, 8, 16, 32, 64,
|
||||
128\}$ (powers of 2), which form a Sidon set because all pairwise sums
|
||||
are distinct. The Singer construction provides optimal Sidon sets for
|
||||
larger address budgets, and the extremal bounds quantify how much
|
||||
address space a given problem size requires.
|
||||
|
||||
The Erdős Problem 30 conjecture — that $h(N) = \sqrt{N} + O(N^\varepsilon)$
|
||||
— remains open. The Lindström bound $\sqrt{N} + \sqrt[4]{N} + 2$ is the
|
||||
best unconditional upper bound proved here.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Finite set arithmetic:** membership, pairwise sums, cardinality.
|
||||
- **Modular arithmetic:** divisibility, residue classes $\mathbb{Z}/M\mathbb{Z}$.
|
||||
- **Extremal combinatorics:** maximizing set cardinality under combinatorial constraints.
|
||||
- **Cauchy-Schwarz inequality** for the incidence bound.
|
||||
- **Finite field arithmetic:** $\mathbb{F}_p$, $\mathbb{F}_{p^3}$, field traces.
|
||||
- **Linear algebra over finite fields:** subspaces, dimension, rank-nullity.
|
||||
- **Group theory:** cyclic groups, quotient groups, cosets.
|
||||
- **Projective geometry:** Singer's theorem on points and lines in $PG(2, p)$.
|
||||
|
||||
---
|
||||
|
||||
## BraidEigensolid
|
||||
|
||||
### What it does
|
||||
|
||||
Defines an **8-strand braid state** and a **crossing step** operator,
|
||||
then proves two compressor-correctness theorems.
|
||||
|
||||
A **BraidState** consists of 8 strands, each carrying:
|
||||
- A 2D phase accumulator $\mathbf{z}_i = (x_i, y_i) \in \mathbb{Z}^2$
|
||||
(represented in Q16.16 fixed-point).
|
||||
- A slot label $s_i \in \{1, 2, 4, 8, 16, 32, 64, 128\}$ (Sidon labels).
|
||||
- A bracket (crossing weight) with a **kappa** value $\kappa_i$.
|
||||
- A residue $\varepsilon_i$.
|
||||
|
||||
The **crossing step** $\sigma$ pairs adjacent strands $(0,1), (2,3),
|
||||
(4,5), (6,7)$ and applies the braid crossing operator to each pair.
|
||||
The crossing operator merges phase vectors by component-wise addition:
|
||||
$\mathbf{z}_i' = \mathbf{z}_i + \mathbf{z}_j$, and computes a new
|
||||
bracket via an octagonal norm approximation.
|
||||
|
||||
An **eigensolid** is a fixed point: $\sigma(s) = s$, meaning every
|
||||
strand's data is unchanged by the crossing step. This is the DC baseline
|
||||
— the converged state of the braid loop.
|
||||
|
||||
**Theorem 1 (Eigensolid Convergence):** If $\sigma(s)$ is already an
|
||||
eigensolid, then applying $\sigma$ again changes nothing:
|
||||
$\sigma(\sigma(s)) = \sigma(s)$.
|
||||
|
||||
**Theorem 2 (Receipt Invertibility):** The receipt tuple
|
||||
$(C, \sigma, k, \varepsilon_{\text{seq}}, t, \emptyset_{\text{scars}})$
|
||||
bijectively encodes the eigensolid state. Given two eigensolid states
|
||||
with identical receipts, all per-strand residues, the crossing matrix,
|
||||
the slot of strand 7, and the step count are equal.
|
||||
|
||||
A **topological triviality** result is proved under non-saturation:
|
||||
if no phase component is at the fixed-point boundary, then eigensolid
|
||||
states have $\kappa_i = 0$ for all strands (genus-0 layer).
|
||||
|
||||
The module also defines a **torus carrier** enrichment: the 8-strand
|
||||
braid lives on a genus-1 torus $T^2$ with two winding numbers
|
||||
$(a, b) \in H_1(T^2; \mathbb{Z}) \cong \mathbb{Z} \oplus \mathbb{Z}$.
|
||||
|
||||
### Why it does it
|
||||
|
||||
The eigensolid is the compressor's convergence target. Every compressor
|
||||
must prove two things: (1) the braid loop converges (eigensolid
|
||||
convergence), and (2) the receipt encodes the state losslessly (receipt
|
||||
invertibility). Together, these guarantee that the compressed
|
||||
representation — the receipt — can be inverted to recover the original
|
||||
state.
|
||||
|
||||
The torus carrier enriches the planar braid with topological information:
|
||||
winding numbers track how many times the braid wraps around the two
|
||||
fundamental cycles of the torus, which matters for phase-sensitive
|
||||
applications.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Fixed-point iteration:** detecting when $f(x) = x$ for a discrete
|
||||
dynamical system on a finite state space.
|
||||
- **Vector addition in $\mathbb{Z}^2$** with saturating arithmetic.
|
||||
- **Octagonal norm:** $\|z\| = \max(|x|, |y|) + \frac{3}{8}\min(|x|, |y|)$.
|
||||
- **XOR operations** on bit vectors (for slot arithmetic).
|
||||
- **Tuple encoding/decoding:** injective maps between state tuples and
|
||||
receipt tuples.
|
||||
- **Algebraic topology (genus-0 layer):** when a braid has no persistent
|
||||
2-cycles in its crossing graph.
|
||||
- **Torus homology:** $H_1(T^2; \mathbb{Z})$, winding numbers.
|
||||
|
||||
---
|
||||
|
||||
## BraidSpherionBridge
|
||||
|
||||
### What it does
|
||||
|
||||
Proves a **structural correspondence** between two different
|
||||
formalisms of the same physical system:
|
||||
|
||||
1. **SpherionState:** a multi-scale merging and renormalization (MMR)
|
||||
model with mountains, spikes, and an RG flow via $\beta$-steps.
|
||||
2. **BraidState:** 8 strands with crossing steps.
|
||||
|
||||
The correspondence operates at two levels:
|
||||
|
||||
**Type bridge:** The integer-node coordinates of a Mountain's apex map
|
||||
to the phase vector of a BraidStrand via a coordinate-wise encoding:
|
||||
the first two coordinates become the $(x, y)$ components of a 2D phase
|
||||
vector, with nonnegative integer coordinates mapped by exact scaling
|
||||
(factor of $2^{16}$).
|
||||
|
||||
**Operation bridge:** The braid crossing operator on strands $(i, j)$
|
||||
corresponds to the Mountain merge operation on the corresponding pair.
|
||||
Both are linear accumulation in their respective spaces:
|
||||
- Braid crossing: $\mathbf{z}' = \mathbf{z}_i + \mathbf{z}_j$ (phase vector addition).
|
||||
- Mountain merge: $\text{apex}' = \text{apex}_1 + \text{apex}_2$ (coordinate-wise integer addition).
|
||||
|
||||
The encoding preserves addition on nonnegative coordinates, so the
|
||||
merged apex maps to the merged phase vector.
|
||||
|
||||
**Flow correspondence:** After $k$ spikes (mountain merge operations),
|
||||
the step count equals $k$. The receipt dimensions correspond:
|
||||
- Crossing matrix $C$ ↔ basin geometry.
|
||||
- Sidon slack $\sigma$ ↔ merge debt.
|
||||
- Step count $k$ ↔ scale decrement count.
|
||||
- Residual series $\varepsilon_{\text{seq}}$ ↔ void topology (Betti cycles).
|
||||
- Scar absence $\emptyset_{\text{scars}}$ ↔ IR fixed point (no pending merges).
|
||||
|
||||
### Why it does it
|
||||
|
||||
The bridge shows that the braid formalism and the MMR formalism are two
|
||||
views of the same coarse-graining process. The braid view is better for
|
||||
convergence proofs (eigensolid convergence), while the MMR view is
|
||||
better for multi-scale analysis (RG flow). The bridge ensures that
|
||||
receipts produced by one formalism can be interpreted by the other.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Coordinate-wise maps** between $\mathbb{Z}^n$ and fixed-point vectors.
|
||||
- **Additive homomorphisms** on nonnegative integers.
|
||||
- **Graph morphisms** between the crossing graph and the merge graph.
|
||||
- **Monotone counter tracking** across formalisms.
|
||||
- **Structural induction** on spike lists.
|
||||
|
||||
---
|
||||
|
||||
## HachimojiLUT
|
||||
|
||||
### What it does
|
||||
|
||||
Constructs a **virtual lookup-table hierarchy** for classifying
|
||||
equations by their position on a manifold.
|
||||
|
||||
The **phase circle** $\mathbb{Z}/360\mathbb{Z}$ has 360 discrete angular
|
||||
positions. The 8 canonical Hachimoji states occupy the octagon vertices
|
||||
at $\{0°, 45°, 90°, \ldots, 315°\}$.
|
||||
|
||||
Each phase $\theta$ embeds into the 15-sphere $S^{15} \subset \mathbb{R}^{16}$
|
||||
via:
|
||||
|
||||
$$q_1(\theta) = \cos(\theta \cdot \pi/180), \quad q_3(\theta) = \sin(\theta \cdot \pi/180)$$
|
||||
|
||||
with all other coordinates zero. This is a full-period embedding (corrected
|
||||
from an earlier half-period version), and $\cos^2 + \sin^2 = 1$ guarantees
|
||||
unit norm.
|
||||
|
||||
The 8 canonical phases embed to **8 distinct points** on $S^{15}$,
|
||||
forming a regular octagon in the $(q_1, q_3)$-plane. The chord length
|
||||
between adjacent vertices is $2\sin(\pi/8)$.
|
||||
|
||||
The **virtual LUT hierarchy** defines three levels of equation grouping:
|
||||
- **Binary LUT** ($k=2$): how two equations compose (8×8 = 64 entries).
|
||||
- **Codon LUT** ($k=6$): one atomic mathematical operation (Genome18 primitive).
|
||||
- **Genome LUT** ($k=50$): universal function (50-token address space).
|
||||
|
||||
**Stability points** under conjugation $\theta \mapsto -\theta$ are
|
||||
exactly $\{0°, 180°\}$ — the self-complementary (ambidextrous) bases
|
||||
$\Phi$ and $\Omega$.
|
||||
|
||||
### Why it does it
|
||||
|
||||
The Hachimoji LUT answers "where does this equation live?" on the
|
||||
manifold. Each equation's shape (number of variables, operators, depth,
|
||||
quantifiers, relations) classifies to one of 8 regime states, which
|
||||
embeds as a point on $S^{15}$. The LUT hierarchy provides compositional
|
||||
structure: binary composition, atomic operations, and universal functions
|
||||
all reduce to geometry on the sphere.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Modular arithmetic:** $\mathbb{Z}/360\mathbb{Z}$, phase addition.
|
||||
- **Trigonometric functions:** $\cos$, $\sin$, exact values at multiples of $\pi/4$.
|
||||
- **Unit sphere in $\mathbb{R}^{16}$:** norm verification, chord distances.
|
||||
- **Injectivity proofs** for finite maps (8 canonical phases → 8 distinct points).
|
||||
- **Classification functions:** mapping combinatorial parameters to discrete labels.
|
||||
- **Composition tables:** binary operations on finite sets.
|
||||
- **Fixed-point detection** under involutions (conjugation).
|
||||
|
||||
---
|
||||
|
||||
## ChentsovFinite
|
||||
|
||||
### What it does
|
||||
|
||||
Proves the **finite Chentsov theorem** for $n = 8$ outcomes: on the
|
||||
probability simplex $\Delta^7 = \{p \in \mathbb{R}^8 : p_i > 0, \sum p_i = 1\}$,
|
||||
the Fisher information metric is the **unique** Riemannian metric (up to
|
||||
positive constant) that is invariant under all Markov splitting embeddings.
|
||||
|
||||
The **Fisher metric** is:
|
||||
|
||||
$$g_p(X, Y) = \sum_{i=1}^{n} \frac{X_i \cdot Y_i}{p_i}$$
|
||||
|
||||
where $X, Y$ are tangent vectors ($\sum X_i = \sum Y_i = 0$).
|
||||
|
||||
A **Markov splitting embedding** refines one outcome into two
|
||||
sub-outcomes with conditional probabilities $q$ and $1-q$. A metric $g$
|
||||
is **Chentsov-invariant** if:
|
||||
|
||||
$$g_p(X, Y) = g_{f(p)}(f_*X, f_*Y)$$
|
||||
|
||||
for all splitting embeddings $f$, where $f_*$ is the pushforward of
|
||||
tangent vectors.
|
||||
|
||||
The proof proceeds by:
|
||||
|
||||
1. Deriving the **functional equation** for the diagonal factor
|
||||
$H(t) = g_p(e_i - e_0, e_i - e_0)$ when $p_i = t$:
|
||||
$$H(t) = q^2 H(qt) + (1-q)^2 H((1-q)t)$$
|
||||
2. Substituting $K(t) = t \cdot H(t)$ to linearize:
|
||||
$$K(t) = q \cdot K(qt) + (1-q) \cdot K((1-q)t)$$
|
||||
3. Proving $K(t) = K(t/2^n)$ for all $n$, hence $K(rt) = K(t)$ for all
|
||||
positive rationals $r$.
|
||||
4. By continuity and density of $\mathbb{Q}$ in $\mathbb{R}$: $K$ is
|
||||
constant, so $H(t) = c/t$.
|
||||
5. Therefore $g = c \cdot g_{\text{Fisher}}$.
|
||||
|
||||
**Corollary for Hachimoji:** The 8-state manifold has a **canonical
|
||||
metric** — the Fisher metric is forced by the invariance requirement,
|
||||
not an arbitrary choice.
|
||||
|
||||
### Why it does it
|
||||
|
||||
Chentsov's theorem is the mathematical foundation for the Hachimoji
|
||||
geometry. It says that if you demand your metric be invariant under
|
||||
coarse-graining (splitting outcomes), then there is only one possible
|
||||
metric (up to scale). This is why the Fisher metric appears: it is the
|
||||
unique geometric structure compatible with the Markov refinement
|
||||
semantics of the 8-state system.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Probability simplex:** $\Delta^{n-1}$, tangent spaces, basis vectors
|
||||
$e_i - e_j$.
|
||||
- **Riemannian metrics on manifolds:** bilinear forms, positive
|
||||
definiteness, symmetry.
|
||||
- **Markov embeddings:** stochastic matrices, pushforward of tangent vectors.
|
||||
- **Functional equations:** $H(t) = q^2 H(qt) + (1-q)^2 H((1-q)t)$,
|
||||
uniqueness of solutions.
|
||||
- **Real analysis:** continuity, density of $\mathbb{Q}$, limits.
|
||||
- **Permutation invariance:** symmetric group actions on the simplex.
|
||||
|
||||
---
|
||||
|
||||
## DynamicCanal
|
||||
|
||||
### What it does
|
||||
|
||||
Defines a **fluid-dynamics-inspired transport model** on a directed
|
||||
graph, with three execution regimes and a pressure-adaptive canal law.
|
||||
|
||||
The **DIAT encoding** (Dual-Interval Algebraic Transform) represents
|
||||
an integer $n$ as a tuple $(k, a, b, ab, a-b)$ where $k = \lfloor\sqrt{n}\rfloor$,
|
||||
$a = n - k^2$, $b = (k+1)^2 - n$. This captures the "shell" position
|
||||
and asymmetry of $n$ relative to adjacent perfect squares.
|
||||
|
||||
The **Dynamic Canal Law** governs effective resistance:
|
||||
|
||||
$$\lambda_{\text{eff}}(P) = \lambda_0 \left[\sigma + (1 - \sigma) e^{-\xi P}\right]$$
|
||||
|
||||
where $P$ is pressure, $\lambda_0$ is base resistance, $\xi$ is
|
||||
elasticity (pressure sensitivity), and $\sigma$ is saturation (minimum
|
||||
fraction). As pressure increases, resistance decreases exponentially
|
||||
toward $\sigma \lambda_0$.
|
||||
|
||||
Three **execution regimes** govern lane updates:
|
||||
|
||||
1. **Coherent:** stable transport with relaxation and healing.
|
||||
2. **Stressed:** distorted transport with torsion and mismatch accumulation.
|
||||
3. **Throat:** wormhole-like lossy transfer with maximum energy extraction.
|
||||
|
||||
Regime classification is by mismatch and stress thresholds:
|
||||
- Coherent: mismatch $\leq \theta_c$ and stress $\leq \theta_s$.
|
||||
- Throat: mismatch $\geq \theta_t$ and edge is a throat.
|
||||
- Stressed: everything else.
|
||||
|
||||
The **canal section** (fluid mode) tracks density, capacity, flux,
|
||||
pressure, compliance, and roughness, with coarse-graining that reduces
|
||||
precision as loop iterations increase.
|
||||
|
||||
All operations are proved **total** (every Q16.16 operation produces a
|
||||
result; no partial functions).
|
||||
|
||||
### Why it does it
|
||||
|
||||
The Dynamic Canal provides a physics-motivated model for adaptive
|
||||
transport on graphs. The canal law captures the intuition that
|
||||
"pressure opens the channel" — higher pressure reduces resistance,
|
||||
allowing more flow. The three regimes model different operating
|
||||
conditions: normal operation (coherent), degraded operation (stressed),
|
||||
and catastrophic transfer (throat). The coarse-graining mechanism
|
||||
trades precision for throughput as iterations accumulate.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Directed graphs:** nodes, edges, edge attributes.
|
||||
- **Saturating arithmetic** on a bounded interval $[-2^{15}, 2^{15}-1]$.
|
||||
- **Exponential decay:** $e^{-\xi P}$ in fixed-point.
|
||||
- **Piecewise-linear regime classification** by threshold comparison.
|
||||
- **Conservation laws:** density = inflow - outflux - siphon.
|
||||
- **Coarse-graining maps:** precision reduction functions parameterized
|
||||
by iteration count.
|
||||
- **Square root and integer decomposition** (DIAT encoding).
|
||||
|
||||
---
|
||||
|
||||
## Schema
|
||||
|
||||
### What it does
|
||||
|
||||
Defines a **wire-level schema** as a type class with two fields:
|
||||
- `byteSize`: the number of bytes in the wire representation.
|
||||
- `wellFormed`: a predicate that must hold for valid values.
|
||||
|
||||
Instances are provided for `UInt8` (1 byte), `Bool` (1 byte),
|
||||
`UInt32` (4 bytes), `UInt64` (8 bytes), `Q16_16` (4 bytes), and
|
||||
`Q0_16` (2 bytes).
|
||||
|
||||
### Why it does it
|
||||
|
||||
The schema is the bridge between mathematical types and their byte-level
|
||||
representations. Every type that can be serialized has a schema that
|
||||
declares its wire size and a well-formedness check. This is the
|
||||
foundation for the wire format and receipt encoding.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Type-theoretic maps** from abstract types to natural numbers
|
||||
(byte sizes).
|
||||
- **Predicates** on types (well-formedness).
|
||||
- **Finite type enumeration** (the set of supported types).
|
||||
|
||||
---
|
||||
|
||||
## WireFormat
|
||||
|
||||
### What it does
|
||||
|
||||
Defines a **wire format** as a certified encode/decode cycle for a
|
||||
type under a layout (row-major or columnar).
|
||||
|
||||
A WireFormat for type $\alpha$ under layout $L$ consists of:
|
||||
- An **encode** function: $\alpha \to \text{ByteArray}$.
|
||||
- A **decode** function: $\text{ByteArray} \to \text{Option}(\alpha)$.
|
||||
- A **size proof:** $|\text{encode}(a)| = \text{byteSize}(\alpha)$ for all $a$.
|
||||
- A **roundtrip proof:** $\text{decode}(\text{encode}(a)) = a$ for all $a$.
|
||||
|
||||
The roundtrip property is the mathematical content: encoding is injective,
|
||||
and decoding is its left inverse.
|
||||
|
||||
### Why it does it
|
||||
|
||||
The wire format ensures that mathematical values can be losslessly
|
||||
serialized to bytes and back. The roundtrip proof guarantees that no
|
||||
information is lost in the encoding — the receipt's byte representation
|
||||
is a faithful encoding of the mathematical state.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Injective maps** from abstract types to byte sequences.
|
||||
- **Left inverses:** proving $f^{-1} \circ f = \text{id}$.
|
||||
- **Length functions** on byte sequences.
|
||||
- **Layout permutations:** row-major vs. columnar ordering of fields.
|
||||
|
||||
---
|
||||
|
||||
## Receipt
|
||||
|
||||
### What it does
|
||||
|
||||
Defines a **receipt** as a 5-tuple:
|
||||
$$R = (\text{gateType},\; \text{cost},\; \text{invariant},\; \text{timestamp},\; \text{wellFormed})$$
|
||||
|
||||
where:
|
||||
- `gateType` $\in \{\text{encode}, \text{decode}, \text{compose}, \text{validate}, \text{transform}\}$.
|
||||
- `cost` $\in \mathbb{Q}_{16.16}$ (fixed-point cost).
|
||||
- `invariant` $\in \Sigma^*$ (string describing what was preserved).
|
||||
- `timestamp` $\in \mathbb{N}$ (monotone nonce for ordering).
|
||||
- `wellFormed` $\in \{0, 1\}$.
|
||||
|
||||
Predicates include:
|
||||
- **Validity:** well-formedness flag is true.
|
||||
- **Positive cost:** cost $> 0$.
|
||||
- **Shared invariant:** two receipts preserve the same property.
|
||||
|
||||
### Why it does it
|
||||
|
||||
The receipt is the unit of attestation in SilverSight. Every gate
|
||||
(encode, decode, compose, validate, transform) produces a receipt
|
||||
proving it completed successfully. The cost field enables resource
|
||||
accounting. The invariant field records what property was preserved.
|
||||
The timestamp enables causal ordering.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **5-tuples** over mixed types (enum, fixed-point, string, natural, boolean).
|
||||
- **Comparison operators** on each component.
|
||||
- **String equality** for invariant matching.
|
||||
|
||||
---
|
||||
|
||||
## Bind
|
||||
|
||||
### What it does
|
||||
|
||||
Defines **receipt composition** as a binary operation:
|
||||
|
||||
$$\text{bind}(R_1, R_2) = (\text{compose},\; c_1 + c_2,\; I_1 \wedge I_2,\; \max(t_1, t_2),\; w_1 \wedge w_2)$$
|
||||
|
||||
where costs add, invariants conjoin (with "$\wedge$" separator),
|
||||
timestamps take the maximum, and well-formedness is the logical AND.
|
||||
|
||||
Proved properties:
|
||||
- **Well-formedness preservation:** $\text{bind}(R_1, R_2)$ is
|
||||
well-formed iff both $R_1$ and $R_2$ are well-formed.
|
||||
- **Cost additivity:** $\text{cost}(\text{bind}(R_1, R_2)) =
|
||||
\text{cost}(R_1) + \text{cost}(R_2)$.
|
||||
- **Timestamp commutativity:** $\max(t_1, t_2) = \max(t_2, t_1)$.
|
||||
- **Associativity of well-formedness:**
|
||||
$\text{wf}(\text{bind}(\text{bind}(a,b),c)) =
|
||||
\text{wf}(\text{bind}(a,\text{bind}(b,c)))$.
|
||||
- **Gate type:** bind always produces a compose gate.
|
||||
|
||||
### Why it does it
|
||||
|
||||
Bind is the fundamental composition primitive for the receipt ledger.
|
||||
It allows chaining verification steps: if gate $A$ produces receipt
|
||||
$R_1$ and gate $B$ produces receipt $R_2$, then $\text{bind}(R_1, R_2)$
|
||||
is a single receipt attesting that both gates completed. The additive
|
||||
cost model enables resource accounting across chains. The conjunction
|
||||
of invariants tracks which properties are preserved by the composite
|
||||
operation.
|
||||
|
||||
### Pure math version
|
||||
|
||||
A graph calculator would need:
|
||||
|
||||
- **Binary operations** on 5-tuples.
|
||||
- **Addition** on fixed-point numbers.
|
||||
- **String concatenation** with a separator.
|
||||
- **Maximum** on natural numbers.
|
||||
- **Logical AND** on booleans.
|
||||
- **Associativity verification** for each component.
|
||||
|
||||
---
|
||||
|
||||
## Summary Table
|
||||
|
||||
| Module | Core Mathematical Object | Key Theorem |
|
||||
|--------|------------------------|-------------|
|
||||
| SidonSets | Sidon ($B_2$) sets in $\mathbb{Z}$ | Singer construction: $\exists$ Sidon mod $p^2+p+1$ of size $p+1$ |
|
||||
| BraidEigensolid | 8-strand braid with crossing step | Eigensolid convergence + receipt invertibility |
|
||||
| BraidSpherionBridge | Morphism between SpherionState and BraidState | Phase vector ↔ apex coordinate correspondence |
|
||||
| HachimojiLUT | Phase circle $\mathbb{Z}/360\mathbb{Z}$ embedded in $S^{15}$ | 8 canonical phases are distinct; stability points = $\{0°, 180°\}$ |
|
||||
| ChentsovFinite | Fisher metric on $\Delta^7$ | Unique Chentsov-invariant metric = $c \cdot g_{\text{Fisher}}$ |
|
||||
| DynamicCanal | Canal law $\lambda_{\text{eff}}(P) = \lambda_0[\sigma + (1-\sigma)e^{-\xi P}]$ | Totality of all operations |
|
||||
| Schema | Type → byte-size map | Byte sizes are nonnegative |
|
||||
| WireFormat | Certified encode/decode cycle | Roundtrip: $\text{decode} \circ \text{encode} = \text{id}$ |
|
||||
| Receipt | 5-tuple attestation record | Validity = well-formedness |
|
||||
| Bind | Binary receipt composition | Associativity on well-formedness; cost additivity |
|
||||
|
|
@ -1,2 +1,11 @@
|
|||
/-! # CoreFormalism.FixedPoint (Stub)
|
||||
|
||||
Redirect module. The canonical Q16_16 fixed-point type and arithmetic live in
|
||||
`SilverSight.FixedPoint`. This file exists solely as a re-export so that
|
||||
`CoreFormalism.FixedPoint` resolves without error; it contains no definitions
|
||||
of its own.
|
||||
|
||||
All consumers should import `SilverSight.FixedPoint` directly.
|
||||
-/
|
||||
/- Duplicate removed per AGENTS.md. Use SilverSight.FixedPoint instead. -/
|
||||
import SilverSight.FixedPoint
|
||||
|
|
|
|||
|
|
@ -45,6 +45,30 @@ import Mathlib.Data.Finset.Basic
|
|||
import Mathlib.Algebra.BigOperators.Basic
|
||||
import Mathlib.Tactic
|
||||
|
||||
/-! # Hermite–Kampé de Fériet Polynomial → Sieve Bridge (PVGS-DQ Bridge §2)
|
||||
|
||||
Connects generalized Hermite–Kampé de Fériet (H-KdF) polynomials to the repunit
|
||||
sieve for Goormaghtigh collision detection. The diagonal H-KdF polynomial's zero
|
||||
set encodes lattice points where repunit collisions R(x,m) = R(y,n) can occur;
|
||||
within the BMS bounds, only the two known Goormaghtigh solutions survive.
|
||||
|
||||
## Key Definitions
|
||||
- `hermitePoly` — two-variable Hermite polynomial H_p(ξ, w)
|
||||
- `Hkdf` — Hermite–Kampé de Fériet polynomial H_{m,n}(x,y;z,u|t)
|
||||
- `sieveCondition` — diagonal H-KdF vanishing at (x,−1,x,−1,1/2) = 0
|
||||
- `repunit` — R(x,m) = (x^m − 1)/(x − 1)
|
||||
|
||||
## Key Theorems
|
||||
- `bms_implies_sieve` — BMS region implies sieve condition (sorry: 979-case enumeration)
|
||||
- `sieve_discriminates_correct` — sieve + collision → Goormaghtigh solutions
|
||||
- `hermite_sieve_isomorphism` — main result: H-KdF sieve ↔ repunit collision structure
|
||||
- `repunit_strictMono_exponent` / `repunit_lower_bound` — arithmetic auxiliaries
|
||||
|
||||
## Dependencies
|
||||
- Mathlib (Nat, Rat, Finset, BigOperators, Tactics)
|
||||
- Axioms: `bms_bounds`, `goormaghtigh_conditional` (imported from GoormaghtighEnumeration in full project)
|
||||
-/
|
||||
|
||||
-- ---------------------------------------------------------------------------
|
||||
-- §0 NOTATION AND PRELIMINARIES
|
||||
-- ---------------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -66,6 +66,31 @@ import Mathlib.Data.Real.Sqrt
|
|||
import Mathlib.Algebra.Order.Positive.Field
|
||||
import Mathlib.Tactic
|
||||
|
||||
/-! # Quantum Sensing Interpretation (PVGS-DQ Bridge §5)
|
||||
|
||||
Formalizes the quantum-state-discrimination interpretation of the PVGS-DQ bridge.
|
||||
Photon-Added Gaussian States (PVGSs) achieve strictly lower Helstrom error than
|
||||
pure Gaussian states for minimum-error quantum discrimination, proving the
|
||||
non-Gaussian advantage. Connects repunit distinguishability to the BMS/Goormaghtigh
|
||||
number-theoretic bounds.
|
||||
|
||||
## Key Definitions
|
||||
- `PVGSParams` — parameterization (α, ζ, k) for photon-added Gaussian states
|
||||
- `gaussianInnerProduct` / `pvgsInnerProduct` — state overlap formulas
|
||||
- `helstromBound` — minimum error probability for quantum state discrimination
|
||||
- `pvgsAdvantage` — PVGS vs Gaussian discrimination advantage
|
||||
- `repunitInnerProduct` — quantum-sensing overlap between repunit states
|
||||
|
||||
## Key Theorems
|
||||
- `pvgs_always_better` — PVGS strictly outperforms Gaussian for k > 0, p ≠ q
|
||||
- `indistinguishable_implies_no_new_solutions` — contradictory hypothesis (overlap = 1 implies Helstrom = ½ ≠ 0)
|
||||
- Supporting lemmas: `pvgs_le_gaussian_overlap`, `pvgs_lt_gaussian_overlap_of_k_pos`, `helstrom_nonneg`, `helstrom_le_half`, `pvgsAdvantage_nonneg`
|
||||
|
||||
## Dependencies
|
||||
- Mathlib (Nat, Rat, Real, Sqrt, Tactics)
|
||||
- Standalone `repunit` and `bms_bounds` axiom (shared with §2)
|
||||
-/
|
||||
|
||||
-- ---------------------------------------------------------------------------
|
||||
-- §0 NOTATION AND PRELIMINARIES
|
||||
-- ---------------------------------------------------------------------------
|
||||
|
|
|
|||
50
formal/SilverSight/PIST/SpectralWitness.lean
Normal file
50
formal/SilverSight/PIST/SpectralWitness.lean
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
-- Spectral witness for BMCTE eigensolid at p/N=1/7
|
||||
-- Phase 2 superconductor H*/Hc₂ ratios (0.135, 0.141, 0.152) form signature matrix
|
||||
|
||||
import SilverSight.PIST.Spectral
|
||||
open SilverSight.PIST.Spectral
|
||||
open SilverSight.FixedPoint.Q16_16
|
||||
|
||||
/-! # Spectral Witness for BMCTE Eigensolid
|
||||
|
||||
Constructs the 8×8 diagonal signature matrix from Phase 2 superconductor
|
||||
H*/Hc₂ ratios (Kondov1999: 0.135, Ju89 YBCO: 0.141, Fasolo2001 Nb: 0.152)
|
||||
scaled to Q16_16 raw integers, then computes its spectral profile to witness
|
||||
the eigensolid transition at p/N ≈ 1/7.
|
||||
|
||||
## Key Definitions
|
||||
- `eigensolidSignatureMatrix` — 8×8 diagonal matrix of H*/Hc₂ ratios as Q16_16 Ints
|
||||
- `eigensolidSpectralProfile` — computed spectral profile (matrix_size, spectral_gap, density)
|
||||
|
||||
## Dependencies
|
||||
- `SilverSight.PIST.Spectral` (SpectralProfile, computeSpectral)
|
||||
- `SilverSight.FixedPoint.Q16_16` (Q16_16 integer scaling)
|
||||
-/
|
||||
|
||||
/-
|
||||
§1 8x8 signature matrix from Phase 2 superconductors
|
||||
|
||||
H*/Hc₂ ratios (scaled to Int):
|
||||
0.135 × 65536 = 8704
|
||||
0.141 × 65536 = 9088
|
||||
0.152 × 65536 = 9984
|
||||
|
||||
Matrix structure: adjacency of H*/Hc₂ values across materials
|
||||
Spectral gap at ~1/7 indicates eigensolid transition.
|
||||
-/
|
||||
|
||||
def eigensolidSignatureMatrix : Array (Array Int) :=
|
||||
#[[8704, 0, 0, 0, 0, 0, 0, 0], -- Kondov1999: H*/Hc₂ = 0.135
|
||||
[0, 9088, 0, 0, 0, 0, 0, 0], -- Ju89 YBCO: H*/Hc₂ = 0.141
|
||||
[0, 0, 9984, 0, 0, 0, 0, 0], -- Fasolo2001 Nb: H*/Hc₂ = 0.152
|
||||
[0, 0, 0, 8704, 0, 0, 0, 0], -- ...
|
||||
[0, 0, 0, 0, 9088, 0, 0, 0],
|
||||
[0, 0, 0, 0, 0, 9984, 0, 0],
|
||||
[0, 0, 0, 0, 0, 0, 8704, 0],
|
||||
[0, 0, 0, 0, 0, 0, 0, 9088]]
|
||||
|
||||
-- Witness
|
||||
def eigensolidSpectralProfile : SpectralProfile := computeSpectral eigensolidSignatureMatrix
|
||||
#eval eigensolidSpectralProfile.matrix_size
|
||||
#eval eigensolidSpectralProfile.spectral_gap
|
||||
#eval eigensolidSpectralProfile.density
|
||||
|
|
@ -12,6 +12,29 @@ import SilverSight.FixedPoint
|
|||
import SilverSight.RRCLogogramProjection
|
||||
import SilverSight.RRC.Emit
|
||||
|
||||
/-! # Receipt Density Scoring (RRC)
|
||||
|
||||
Ports the receipt-density scoring logic from Research Stack's
|
||||
`Semantics.RRC.ReceiptDensity` into SilverSight. Computes a weighted
|
||||
density and confidence score from status, axis flags, spectral features,
|
||||
and PIST shape agreement — all in Q16_16 fixed-point arithmetic.
|
||||
|
||||
This module is an **admissibility gate**, not a proof. Promotion is
|
||||
always `not_promoted` at this stage.
|
||||
|
||||
## Key Definitions
|
||||
- `SourceStatus` / `statusScore` — base score from row status (BLOCKED→VERIFIED)
|
||||
- `AxisFlags` / `axisScore` — target-axis hit ratio (5 boolean flags, capped at 4)
|
||||
- `SpectralFeatures` / `spectralQuality` — weighted spectral quality composite
|
||||
- `shapeAgreement` — PIST proxy/exact shape match scoring
|
||||
- `computeDensity` — final weighted density + confidence + warnings
|
||||
|
||||
## Dependencies
|
||||
- `SilverSight.FixedPoint` (Q16_16 arithmetic)
|
||||
- `SilverSight.RRCLogogramProjection` (RRCShape type)
|
||||
- `SilverSight.RRC.Emit` (emission boundary)
|
||||
-/
|
||||
|
||||
namespace SilverSight.RRC.ReceiptDensity
|
||||
|
||||
open SilverSight.FixedPoint
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue