From 89b8f4b243ff31dedf0b661391ca60bc0d4ce8a0 Mon Sep 17 00:00:00 2001 From: allaun Date: Fri, 26 Jun 2026 23:41:14 -0500 Subject: [PATCH] docs: standalone Cold Reviewer Protocol document Explicit two-gate protocol (Arithmetic + Structural) with step-by-step calculator verification for each invariant. Covers goals, methodology, extension rules, and decision procedure. --- docs/reviews/COLD_REVIEWER_PROTOCOL.md | 389 +++++++++++++++++++++++++ 1 file changed, 389 insertions(+) create mode 100644 docs/reviews/COLD_REVIEWER_PROTOCOL.md diff --git a/docs/reviews/COLD_REVIEWER_PROTOCOL.md b/docs/reviews/COLD_REVIEWER_PROTOCOL.md new file mode 100644 index 00000000..b52f8751 --- /dev/null +++ b/docs/reviews/COLD_REVIEWER_PROTOCOL.md @@ -0,0 +1,389 @@ +# 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\) |