Archive PURE_MATH_DESCRIPTION.md

archive/2026-07-02/docs/PURE_MATH_DESCRIPTION.md

@@ -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 |