land(mirrormere): the six verified team branches, integrated serially (4 proofs + 4 emitter kinds)

telperion/README.md

@@ -168,6 +168,7 @@ under [`examples/`](examples/).
 | `IntervalGramInertiaEmitter` | the **exact inertia of an INTERVAL matrix**: for a rational box `lo ≤ G ≤ hi`, EVERY real symmetric `G` inside it has signature exactly `(p, q)` — `RHLinalg.posIndex hG = p ∧ RHInertia.defect hG = q`. Untrusted Python computes the midpoint `M`, an exact rational congruence `BᵀMB = D` (symmetric Gaussian elimination with pivoting — `psd_form`'s LDLᵀ primitive run to a full diagonalization), and the witness bases `X` (positive pivots) / `Y` (negative pivots) rescaled to unit column absolute-sum; the box is absorbed by `|xᵀ(G−M)x| ≤ w·(Σ|xᵢ|)²` and Cauchy–Schwarz, so the certificate is sound exactly when the pivot margin beats the slack, `w·S < δ`. Fills the gap `psd_form` (one explicit matrix, definite only), `rayleigh_gram` (one direction) and `hermitian_moment` (scalar shadows) leave open — the D2/D3/T3 shape "this Arb-enclosed Hermitian matrix has negative index exactly q". REFUSES an asymmetric/empty box (the phantom: no Hermitian matrix in it), a singular midpoint, a definite box (that is `psd_form`), and any box wider than the pivot margin. **Island-pinned** to the ported RHLinalg block (v4.32.0); real-symmetric only | per-entry `inertia_entries` + `linarith only` for the box, `nlinarith` for the compressed margin, then RHInertia's `compress_posDef_of_interval` + `inertia_eq_of_witnesses` (Sylvester both ways) |
 | `BraggAmplitudeEmitter` | a **certified truncated diffraction sum** `Σ_k cos(γ_k·u) ∈ [A,B]` over rational ordinate brackets `[a_k,b_k]` at a rational Bragg frequency `u` (PROGRAM ANDÚRIL × MIRRORMERE). The `BraggH100` `CosEnclosure` pipeline reduced to a small base-case instance (3–5 ordinates, `|c_k|≤1`): a per-ordinate cos box (order-4 Taylor bracket + Lipschitz width absorption) folded by `add_encl`, PER-ZERO LEMMA SPLIT. Refuses a claimed `[A,B]` that does not enclose the folded box (negative control) or an out-of-range sample `|c_k|>1` | per-box `CosEnclosure.cos_base_interval` + `cos_encl_bracket` (`norm_num`/`nlinarith`); fold `CosEnclosure.add_encl` + `linarith` |
 | `DefectWitnessEmitter` | the **two-configuration inertia gap** (MIRRORMERE `BraggDefect`): on-line defect functional `q(0)=0 ∈ [A,B]`, off-line `q(d)=−d² ∈ [−d_hi²,−d_lo²]` strictly `< 0` for excess `d ∈ [d_lo,d_hi]`, and the **leakage gap** `−d_lo² < 0 = q(0)` — the Alpöge–Furman signature-(1,1) leakage as a kernel-observable separation. Self-contained on the given rational excess bracket (no Arb `exp` hypothesis). Refuses a degenerate/swapped configuration `d_lo=0` (no excess) or `0 ∉ [A,B]` | `unfold` + `norm_num`/`nlinarith` (three theorems: online / offline / leakage_gap) |
+| `ExpEnclosureEmitter` | a **certified rational bracket of a transcendental exponential** at a rational point (MIRRORMERE): `lo ≤ Real.exp x ≤ hi` for `|x| ≤ 1`, plus the `exp_neg`, **deficit** (`lo ≤ e^x + e^{−x} − 2 ≤ hi`, the QC_RECURRENCE row-(a) excess) and `cosh` faces.  The exact rational order-`n` Taylor box of `Real.exp_bound` (`S = Σ_{m<n} x^m/m!`, `r = |x|^n·(n+1)/(n!·n)`) is re-derived in the kernel; the emitter picks the LEAST order whose box fits the CLAIMED bracket.  **Dogfooded**: `exp_tenth_bracket` reproduces `BraggDefect.expLo/expHi` verbatim and discharges the Arb `hexp` hypothesis, giving `bragg_defect_witness_unconditional` (MM_bragg_defect_witness), and the deficit/cosh faces reproduce `excess_bracket` / `ZooDH.cosh_bracket` constants.  Refuses a bracket the Taylor box does not imply (the forge case / negative control), `|x|>1`, order `<1` or `>64`, an inverted bracket, a non-positive deficit displacement, or non-rational input | `Real.exp_bound` + `simp only [Finset.sum_range_succ, Finset.sum_range_zero]` + `norm_num [Nat.factorial]` + `linarith` (two-sided modes fold the two faces; `cosh` via `Real.cosh_eq`) |
 | `SelfInversiveRigidityEmitter` | **equal-modulus real-rootedness** (MIRRORMERE R3, n=2): for Gaussian-rational `c₁,c₂` with `\|c₁\|²=\|c₂\|²` EXACTLY, the two-frequency sum `c₁e^{iλ₁x}+c₂e^{iλ₂x}` is real-rooted — reverse-Dyson rigidity forced by an equal-modulus condition on the coefficients. Applies the in-island `Quasicrystal.twoFreq_realRooted_iff`. Refuses unequal modulus (negative control — every zero then off the real line), a zero coefficient, or `λ₁=λ₂` | `Complex.norm_def` + exact rational `normSq` equality (`norm_num`) fed into `twoFreq_realRooted_iff.mpr` |
 | `WindingBoxZeroEmitter` | **Arb-trust-class winding-number box certificate** for a zero (the `turing_band` sidecar trust class): the rigorous zero count of an analytic `f` on a rational-cornered box via the quadrant-advance argument principle over Arb-ball boundary samples. Ships **no kernel theorem** — a `.cert.json` sidecar (box, edge-sample count, precision, winding integer, `trust_class="arb"`) + a documentation stub honestly stating the trust boundary. Self-check RE-VERIFIES the winding at doubled precision + density; refuses a claimed count the argument principle does not support (negative control) | none (Arb sidecar + doc stub; `nthm=0`) |
 | `CustomAssemblyEmitter` | escape hatch for a hand-designed assembly | your skeleton |
@@ -176,6 +177,8 @@ under [`examples/`](examples/).
 | `LehmerPairEmitter` | **RH Face 5 (de Bruijn–Newman / criticality).** A certified *Lehmer pair* — two consecutive ζ-zeros anomalously close (Face 5: RH ⟺ Λ ≤ 0, Λ ≥ 0 by Rodgers–Tao): from Arb-certified ordinates (`hardy_z_zeros`) the exact rational quality `δ²·C_n` (`C_n` = neighboring-zero curvature) is emitted as `quality_short ≤ qcap < 1`, the anomalous-closeness signature. Ships the WIP Λ-bound skeleton `lehmer_lambda_bound_wip` (the CNV Λ-lower-bound constant is UNVERIFIED this pass, carried as hypothesis, no numeric kernel claim) + `lehmer_neg_refutes`. Refuses a non-Lehmer pair (quality ≥ 1) or `qcap` below the quality / ≥ 1 | `by norm_num` on the exact-rational quality inequality; the Λ-bound WIP skeleton is `le_trans hround hCNV` |
 | `BagchiRecurrenceEmitter` | **RH Face 4 (recurrence).** A finite recurrence observation (Bagchi 1981: RH ⟺ ζ strongly recurrent in the strip): over a compact rational box K (a σ×t grid inside `1/2 < Re s < 1`) and a shift τ, the certified grid-max `M = max_grid |ζ(s+iτ) − ζ(s)|` (each per-point deviation a rigorous flint/Arb `acb.zeta` `abs_upper`) satisfies `M ≤ ε`; `M` carried as hypothesis `hdev`, `ε` a readable rounded-up cap. Ships `bagchi_recurrence_refutes`. Arb-trust class; scope = sup over the GRID (continuous sup needs a modulus argument, documented not claimed). Refuses `ε < M` or an empty grid. A finite observation, NOT RH | `le_trans hdev (by norm_num)` — the Arb grid-max carried as hypothesis, `M ≤ ε` closed by `norm_num` |
 
+| `ExpLaurentIdentityEmitter` | **RH Face 4 <-> Face 1 dictionary bookkeeping.** An identity in `Real.exp d` and `Real.exp (-d)` -- amplitude sums `e^d + e^(-d)` (a `2 cosh` channel), one-sided clearances `e^d - 1` / `1 - e^(-d)`, their products and squares -- certified as an EXACT reduction of `lhs - rhs` modulo the single relation `e^d * e^(-d) = 1` in `Q[y, z]`; the quotient (cofactor) is the load-bearing certificate. Refuses a nonzero remainder (the motivating case: the clearances' SUM is `2d + O(d^3)`, NOT the amplification excess -- QC_RECURRENCE section 6's own corrected mistake) and refuses a cofactor-0 plain ring identity (that shape is `IdentityEmitter`'s). Unconditional, zeta-free; dictionary bookkeeping, NOT an analytic theorem and NOT a step toward RH | `have hrel : Real.exp d * Real.exp (-d) = 1 := by rw [<- Real.exp_add]; norm_num` then `linear_combination (cofactor) * hrel` |
+
 *Candidate (not-yet-built) shapes are tracked in the emitter roadmaps under
 [`docs/`](docs/) — `EMITTER_ROADMAP_2026-08-21.md` (BG / P=NP backlog: `SymmetricQuadForm`,
 `PolytopeMaxMonotone`, `SingularPSD`, …), `EMITTER_ROADMAP_2026-09-02_RH_CROSSCUT.md`

telperion/docs/EMITTER_MIRRORMERE_2026-09-18.md

@@ -0,0 +1,98 @@
+# MIRRORMERE emitter additions -- 2026-09-18
+
+conjecture1_proved = False.  Nothing in this document, and nothing emitted by the tools it
+describes, is progress toward RH.  Each entry is a finite, unconditional, kernel-checked
+fact, and several of them are explicitly NEGATIVE controls: they certify that a hoped-for
+property FAILS at finite truncation.
+
+## `twofreq_offline` -- certified OFF-line displacement of a two-frequency section
+
+**Module** `telperion/src/telperion/emit_twofreq_offline.py` ·
+**Emitter** `TwoFreqOfflineEmitter` ·
+**Dogfood** `telperion/examples/twofreq_offline/generate.py` ->
+`examples/quasicrystal/lean/EulerFactorSectionOffline.lean` ·
+**CI** `twofreq-offline-compiles` ·
+**Adapter** `negctrl_adapters/adapter_twofreq_offline.py` ·
+**Stance** `STRUCTURALLY_NONVACUOUS` + `NEG_CONTROL_ADAPTER`.
+
+### The shape
+
+The quasicrystal island proves (`TwoFreqRigidity.lean:92`, v4.32)
+
+```
+twoFreq_realRooted_iff :
+  c1 != 0 -> c2 != 0 -> lam1 != lam2 ->
+  ((forall x : C, twoFreq c1 c2 lam1 lam2 x = 0 -> x.im = 0) <-> ||c1|| = ||c2||)
+```
+
+`selfinversive_rigidity` (2026-09-14) emits the POSITIVE direction: `|c1|^2 = |c2|^2`
+EXACTLY, hence real-rooted.  `twofreq_offline` emits the NEGATIVE direction: `|c1|^2 !=
+|c2|^2` EXACTLY, hence NOT real-rooted -- some zero lies strictly off the real line.
+
+The two emitters **partition the coefficient space**.  Each REFUSES precisely the regime
+the other certifies (`selfinversive_rigidity` refuses unequal modulus; `twofreq_offline`
+refuses equal modulus), so neither can emit a false theorem, and the pair of refusals is
+the anti-phantom guard for both.
+
+### Why it was needed
+
+`MM_euler_factor_section_offline` (ladder rung T2, `QC_TORUS_SECTION_LADDER_MEMO`
+sections 4b/5) is exactly the negative direction at the `p = 2` Euler factor, and its
+coefficient is the IRRATIONAL `-1/sqrt 2` -- which the Gaussian-rational-only
+`selfinversive_rigidity` emitter cannot take.  So the emitter adds:
+
+* three coefficient literal shapes with EXACT rational moduli --
+  `gauss(re, im)` (`|c|^2 = re^2 + im^2`), `inv_sqrt(s, sign)` (`|c|^2 = 1/s`),
+  `real_sqrt(q, s)` (`|c|^2 = q^2 s`);
+* two frequency literal shapes -- `rat(r)` and `neglog(p)` (the literal `-(Real.log p)`).
+
+That turns the single registry node into the whole T2 FAMILY: for every `p >= 2`, the
+Euler factor `1 - p^(-s)` read on `s = 1/2 + i x` is the section
+`twoFreq 1 (-(1/sqrt p)) 0 (-(log p))`, whose moduli `1` and `1/sqrt p` never agree.
+
+### What each instance emits
+
+1. `{nm}` -- `NOT (forall x : C, twoFreq c1 c2 lam1 lam2 x = 0 -> x.im = 0)`;
+2. `{nm}_offline_zero` -- the existence corollary `exists x, ... = 0 AND x.im != 0`;
+3. `{nm}_displacement` (mode `displacement`, Euler-factor shape ONLY) -- the certified
+   LOCATION: `forall x, ... = 0 -> x.im = 1/2`, i.e. every zero sits on `Re s = 0`,
+   uniformly, with no dependence on the truncation.
+
+### Refusals (all EXACT rational arithmetic, no floats)
+
+`|c1|^2 == |c2|^2` (the sum IS real-rooted -- the emitted negation would be FALSE); a zero
+coefficient; `lam1 == lam2` including the disguised `neglog(1) == rat(0)` (log 1 = 0); a
+negative rational frequency opposite a `-log p` frequency (the emitted separation is
+`-log p < 0 <= r`); a radicand that is not an integer `>= 2`; `mode='displacement'`
+outside the Euler-factor shape (the general displacement is
+`-log(|c1|/|c2|) / (lam2 - lam1)`, not `1/2` -- refused rather than guessed); `p < 2`.
+
+### Negative control
+
+`adapter_twofreq_offline` forges the `selfinversive_rigidity` TRUE instance
+(`c1 = 3/5 + 4/5 i`, `c2 = 1`, equal moduli 1) by hand-minting the frozen dataclass, thus
+bypassing the Layer-1 refusal.  The forged proof reaches `h2 : (1 : R) = 1` with goal
+`False` and the kernel rejects it (observed: `unsolved goals ... h2 : True |- False`).  The
+true twin -- the `p = 2` Euler factor, moduli 1 vs 1/2 -- compiles clean.  Both twins are
+rendered in BRIDGE-HYPOTHESIS mode (the island `twoFreq` copied verbatim into the prelude,
+the island iff carried as an explicit hypothesis `hiff`), because the harness elaborates
+against plain `import Mathlib`; the same discipline as `adapter_bragg_floor`.  The
+hypothesis-FREE island theorem is what the `twofreq-offline-compiles` CI job builds.
+
+### Verification performed (2026-09-18, local, v4.32 quasicrystal island)
+
+* `lake build EulerFactorSectionOffline` -- green, 8 theorems, no warnings;
+* `#print axioms` on all 8 -- `[propext, Classical.choice, Quot.sound]`;
+* `telperion.statement_match.statement_match_check` -- 2/2 match, so
+  `euler_factor_section_offline` and its displacement companion state EXACTLY the intended
+  propositions (kernel-level defeq, not string containment);
+* `generic_negative_control` against the island env -- `kernel_rejects=True`,
+  `true_compiles=True`, `okay=True`.
+
+### Honest scope
+
+A finite fact about ONE Euler factor at a time.  It says nothing about zeta, about the
+Euler product, or about RH.  Read positively it is a WARNING: per-rung line membership
+genuinely fails, at every rung and every prime, with a uniform displacement of 1/2, so
+critical-line membership can only ever be an infinite-N continuation phenomenon -- never a
+finite-section fact.  conjecture1_proved = False.