# Cold Reviewer Protocol

**A formal verification protocol for independently checking mathematical
claims using only discrete, calculator-verifiable computation.**

---

## 1. Goals

### Primary goal

Enable a reviewer with **no domain expertise** (no Lean, no braid theory,
no Temperley–Lieb algebras, no differential geometry) to independently
determine whether the core claims of the Unified Covariant Field Theory
are mathematically sound.

### Secondary goals

1. **Isolate domain knowledge.**  All expert-level claims (geometric
   conjectures, spectral theory, tensor categories) are explicitly gated
   behind the discrete arithmetic layer.  A reviewer who passes the
   Arithmetic Gate has already validated the foundation without needing
   to understand the superstructure.

2. **Eliminate tautologies.**  Every invariant must be checked against
   independent calculation, not against another statement in the same
   manuscript.  No invariant may depend on another invariant.

3. **Produce a bounded receipt.**  A reviewer's final pass/fail verdict
   is a binary decision: all four invariants hold and no structural red
   flag is present ⟶ **PASS**.  Otherwise ⟶ **FAIL**.

4. **Provide a formal upgrade path.**  Each invariant maps directly to a
   Lean theorem verified by `norm_num` or `dec_trivial`.  A reviewer who
   trusts the Lean kernel can skip manual calculation and run
   `lake build SilverSight` (3307 jobs, 0 errors).

---

## 2. The Two-Gate Structure

```
┌────────────────────────────────────────────────────────────────────┐
│                    MANUSCRIPT UNDER REVIEW                          │
│  UnifiedCovariant.lean — Unified Covariant Field Theory            │
├────────────────────────────────────────────────────────────────────┤
│                                                                    │
│  GATE A: ARITHMETIC GATE                                           │
│  ────────────────────────                                           │
│  Verify I₁, I₂, I₃, I₄ independently.                              │
│  Reject immediately if any fails.                                  │
│                                                                    │
│  ↓  (all pass)                                                     │
│                                                                    │
│  GATE B: STRUCTURAL GATE                                            │
│  ────────────────────────                                           │
│  Check that none of the three red-flag claims appear anywhere      │
│  in the manuscript.  Reject if any is present.                     │
│                                                                    │
│  ↓  (no red flags)                                                 │
│                                                                    │
│  GATE C: BUILD GATE                                                 │
│  ────────────────────────                                           │
│  (Optional, for Lean-literate reviewers)                            │
│  Run `lake build SilverSight`.  Must report 0 errors.              │
│                                                                    │
│  ↓  (0 errors)                                                     │
│                                                                    │
│                    ✅ VERDICT: PASS                                 │
│  Core discrete claims are sound.  Higher-level geometric claims     │
│  (Layer 3) are deferred but structurally harmless.                 │
└────────────────────────────────────────────────────────────────────┘
```

---

## 3. Gate A — Arithmetic Gate

### Instructions

You need: **a calculator** (or pen and paper, or a Lean kernel).

For each invariant, perform the required computation.  The answer is
predetermined.  If your result matches, the invariant passes.  If your
result differs, **reject the manuscript** — the foundation is unsound.

**DO NOT** skip any invariant.  **DO NOT** accept "by symmetry" or
"by a similar argument" as a substitute for independent calculation.

---

### I₁. Golden-Ratio Identity

**Claim:** \(\phi = \frac{1 + \sqrt{5}}{2}\) satisfies \(\phi^2 - \phi - 1 = 0\).

**How to verify:**

1. Compute \(\sqrt{5} \approx 2.236067977\ldots\)
2. Compute \(1 + \sqrt{5} = 3.236067977\ldots\)
3. Divide by 2: \(\phi = 1.618033988\ldots\)
4. Compute \(\phi^2 = (1.618033988)^2 = 2.618033988\ldots\)
5. Compute \(\phi^2 - \phi - 1 = 2.618033988 - 1.618033988 - 1 = 0\).

**Alternative (exact symbolic):**
\[
\phi^2 - \phi - 1 = \frac{(1+\sqrt{5})^2}{4} - \frac{1+\sqrt{5}}{2} - 1
= \frac{1 + 2\sqrt{5} + 5}{4} - \frac{1+\sqrt{5}}{2} - 1 = 0.
\]

**Lean reference:** `golden_identity` (line 86).

---

### I₂. Fixed-Point Gap

**Claim:**
\[
\sigma = \frac{9984}{65536} = \frac{39}{256},\qquad
\tau = \frac{1}{7},\qquad
\sigma - \tau = \frac{17}{1792} > 0.
\]

**How to verify:**

1. Reduce \(\frac{9984}{65536}\): divide numerator and denominator by 256.
   \[
   \frac{9984}{65536} = \frac{9984 \div 256}{65536 \div 256} = \frac{39}{256}.
   \]
   *(Check: 256 × 39 = 9984, 256 × 256 = 65536. ✓)*

2. Compute the difference with common denominator 1792:
   \[
   \frac{39}{256} - \frac{1}{7} = \frac{39 \times 7}{256 \times 7} - \frac{1 \times 256}{7 \times 256}
   = \frac{273}{1792} - \frac{256}{1792} = \frac{17}{1792}.
   \]

3. Check positivity: \(17 > 0\). ✓

**Also verify:** \(\sigma > \tau\) (since \(17 > 0\)).

**Lean reference:** `spectral_gap_positive` (line 99).

---

### I₃. Fibonacci Values

**Claim:** \(F_7 = 13\) and \(F_8 = 21\).

**How to verify:** Run the recurrence from the definition.

| \(n\) | \(F_n\) | Calculation |
|------|---------|-------------|
| 0 | 0 | (by definition) |
| 1 | 1 | (by definition) |
| 2 | 1 | \(F_0 + F_1 = 0 + 1\) |
| 3 | 2 | \(F_1 + F_2 = 1 + 1\) |
| 4 | 3 | \(F_2 + F_3 = 1 + 2\) |
| 5 | 5 | \(F_3 + F_4 = 2 + 3\) |
| 6 | 8 | \(F_4 + F_5 = 3 + 5\) |
| **7** | **13** | \(F_5 + F_6 = 5 + 8\) |
| **8** | **21** | \(F_6 + F_7 = 8 + 13\) |

Both values match the claim.

**Lean reference:** `fibonacci_dims` (line 106), `fib7_is_13` (line 232).

---

### I₄. Sidon Uniqueness

**Claim:** For \(a,b,c,d \in \{0,1,2,3,4,5,6,7\}\),

\[
2^a + 2^b = 2^c + 2^d \;\Longrightarrow\; \{a,b\} = \{c,d\}.
\]

**How to verify — method 1 (binary expansion):**

1. Write each integer \(2^k\) in binary: it is a 1 followed by \(k\) zeros.
   \[
   2^0 = 1_2,\; 2^1 = 10_2,\; 2^2 = 100_2,\; \ldots,\; 2^7 = 10000000_2.
   \]

2. The sum \(2^a + 2^b\) in binary has:
   - **Case \(a = b\):** a single 1 in position \(a+1\) (carry).
   - **Case \(a \neq b\):** exactly two 1 bits, at positions \(a\) and \(b\).

3. Binary representation is unique.  Therefore if two sums are equal, the
   sets of bit positions must be identical.

**How to verify — method 2 (exhaustion, 8⁴ = 4096 cases):**

Check all quadruples \((a,b,c,d)\).  If \(2^a + 2^b = 2^c + 2^d\) then
\(\{a,b\} = \{c,d\}\).  This is a finite computation.  With a computer:

```python
for a in range(8):
  for b in range(8):
    for c in range(8):
      for d in range(8):
        if 2**a + 2**b == 2**c + 2**d:
          assert {a,b} == {c,d}
```

No counterexample exists.

**Lean reference:** `sidon_unique` (line 110), verified by `dec_trivial`.

---

## 4. Gate B — Structural Gate

### Instructions

Read through the entire manuscript.  If **any** of the following three
claims appears verbatim or in spirit, **reject**.

---

### Red Flag 1: \(J^2 = -I\)

| ✗ WRONG | ✓ CORRECT |
|---------|-----------|
| \(J^2 = -I\) | \(J^2 = J + I\) |

**Why it matters:** \(J = \phi \cdot \mathrm{id}_V\) satisfies the
golden-ratio polynomial \(x^2 - x - 1 = 0\).  Its eigenvalues are
\(\phi\) and \(-1/\phi\), not \(\pm i\).  It is **not** an almost-complex
structure.  Claiming \(J^2 = -I\) would make \(J\) a complex structure on
a real vector space, which changes the entire geometric interpretation.

**How to check:** Find the definition of \(J\) (or `goldenEndomorphism`)
and verify its defining relation.  The correct relation is \(J^2 = J + I\).

---

### Red Flag 2: \(\Delta_7\) is Kähler

| ✗ WRONG | ✓ CORRECT |
|---------|-----------|
| \(\Delta_7\) is Kähler | \(\mathbb{CP}^7\) is Kähler (simplex is 7-real-dimensional, odd) |

**Why it matters:** A Kähler manifold must have even real dimension.
The open simplex \(\Delta_7 = \{p \in \mathbb{R}_{>0}^8 \mid \sum p_i = 1\}\)
has dimension \(8 - 1 = 7\) (odd).  Kähler on \(\Delta_7\) is impossible.

**How to check:** Find any claim that a Kähler structure exists on
\(\Delta_7\) or on a 7-dimensional (or odd-dimensional) manifold.
If the manuscript refers to \(\mathbb{CP}^7\) (real dimension 14) instead,
this red flag is avoided.

---

### Red Flag 3: \(\dim(\mathrm{TL}_7) = 13\)

| ✗ WRONG | ✓ CORRECT |
|---------|-----------|
| \(\dim(\mathrm{TL}_7) = 13\) | \(\dim(\mathrm{TL}_7) = C_7 = 429\) |

**Why it matters:** The \(n\)-th Catalan number is
\[
C_n = \frac{1}{n+1}\binom{2n}{n},
\qquad
C_7 = \frac{1}{8}\binom{14}{7} = \frac{3432}{8} = 429.
\]
The value 13 is the Fibonacci integer \(F_7\), which arises only in the
specialized Temperley–Lieb quotient at \(q = e^{i\pi/5}\) (Fibonacci
anyon model).  Confusing 13 with 429 is a dimension error of factor ~33×,
which invalidates any spectral or geometric argument that depends on it.

**How to check:** Find any claim about \(\dim(\mathrm{TL}_7)\), the
dimension of the Temperley–Lieb algebra on 7 strands.  If it is 13,
reject.  If it is 429 (or the Fibonacci quotient is explicitly named),
this red flag is avoided.

---

## 5. Gate C — Build Gate (Optional)

For reviewers with access to Lean 4 and Mathlib:

```bash
cd /home/allaun/SilverSight
lake build SilverSight
```

**Expected result:** 3307 jobs, 0 errors.

If the build fails, the manuscript has a formalization error.

---

## 6. Extending the Protocol

### Adding a new invariant to Gate A

Every new Layer-1 invariant must satisfy:

1. **Independence.**  No invariant may reference another invariant's
   conclusion.  Each must be checkable from first principles.

2. **Finiteness.**  The verification must be a finite computation:
   rational arithmetic, integer arithmetic, or finite case analysis
   (dec_trivial).  No limits, no infinite series, no analysis.

3. **Lean correspondence.**  Each invariant must have a corresponding
   Lean theorem verified by `norm_num` or `dec_trivial`.

4. **Documentation in this document.**  Add a new subsection with:
   - The exact mathematical claim
   - A step-by-step calculator verification procedure
   - The Lean reference

### Adding a new red flag to Gate B

Every new structural red flag must:

1. Be an **unambiguously wrong statement** that a non-expert could
   plausibly write.
2. Have a clear correction and a brief explanation of why the wrong
   version is harmful.
3. Be listed in the Structural Gate table.

### Adding a new layer

The protocol supports exactly three layers:

| Layer | Content | Gate | Standard |
|-------|---------|------|----------|
| 1 | Discrete foundations | Gate A | 0 sorries |
| 2 | Mechanical theorems | Gate B (transitively) | 0 sorries |
| 3 | Geometric conjectures | Deferred | `sorry` permitted |

A new layer must be assigned to one of these three.  No "Layer 1.5" or
"Layer 2b" may bypass Gate A.  If a claim is not discrete and finite,
it must be Layer 3 or be restated in discrete form.

---

## 7. Decision Procedure

```
For each invariant I₁–I₄:
    verify independently
    if any fails → REJECT (Arithmetic Gate fail)

For each red flag R₁–R₃:
    check manuscript
    if any is present → REJECT (Structural Gate fail)

Optionally:
    run `lake build SilverSight`
    if errors → REJECT (Build Gate fail)

Otherwise → PASS
```

### What PASS means

The four discrete invariants are mathematically sound.  No obvious
structural error is present.  The manuscript is ready for expert review
of the Layer 3 geometric conjectures.

### What FAIL means

The manuscript has a foundational error.  Corrections must be made to
the offending invariant or red flag before any higher-level claims can
be evaluated.

---

## 8. Quick Reference

### Arithmetic Gate (I₁–I₄)

| ID | Claim | Verification | Lean |
|----|-------|-------------|------|
| I₁ | \(\phi^2 - \phi - 1 = 0\) | Expand \((1+\sqrt{5})^2/4\) | `golden_identity` |
| I₂ | \(\sigma - \tau = 17/1792 > 0\) | Common denominator 1792 | `spectral_gap_positive` |
| I₃ | \(F_7 = 13,\; F_8 = 21\) | Run recurrence to term 8 | `fibonacci_dims` |
| I₄ | Sidon uniqueness | Binary expansion uniqueness | `sidon_unique` |

### Structural Gate (Red Flags)

| ID | Wrong claim | Correct |
|----|-------------|---------|
| R₁ | \(J^2 = -I\) | \(J^2 = J + I\) |
| R₂ | \(\Delta_7\) is Kähler | \(\mathbb{CP}^7\) is Kähler |
| R₃ | \(\dim(\mathrm{TL}_7) = 13\) | \(\dim(\mathrm{TL}_7) = C_7 = 429\) |
