Logical loop for RH being True, always.

structure Setting where
  hyp       : Prop
  Prov      : Prop → Prop
  sigma1    : ¬ hyp → Prov (¬ hyp)
  sound_neg : Prov (¬ hyp) → ¬ hyp

The key step is Classical.byContradiction (fun n => h (S.sigma1 n)). So cant_refute_seals, and therefore independence_forces_truth, is the field sigma1 read contrapositively, plus classical logic. The printed cone, [propext, Classical.choice, Quot.sound], is correct, because a structure field is data and does not show up in an axiom cone. The paper does disclose the field in prose ("Σ₁-completeness ... and soundness on the denial, both carried as hypotheses"). But the status box lists the root and the reading, not this field, and the route table shows only the cone.

Two details matter:

• independence_forces_truth takes _hp : ¬ S.Prov S.hyp and never uses it. The theorem needs only non-refutability. Its name says independence, but its content is cannot-refute.
• For ζ, the field's instance is not in the kernel. The paper cites Davis, Matiyasevich and Robinson (1976) and Lagarias (2002) for it, and its own table says ζ "is not formalized." So for RH the premise carries the grade of its citation.

Chain. Let P be "RH holds" (S.hyp) and Q be "ZFC proves ¬RH" (S.Prov (¬ S.hyp)).

1. Field sigma1: ¬P → Q. This is the only non-logical input.
2. Hypothesis hn: ¬Q.
3. Contrapositive of 1: ¬Q → ¬¬P.
4. From 2 and 3: ¬¬P.
5. Classical double negation elimination: P.

So the theorem is the tautology ((¬P → Q) ∧ ¬Q) → P, with sigma1 supplying ¬P → Q. The Lean proof uses only that field and classical contradiction. It does not use _hp.

Premise-free part. The tautology is premise-free. The conclusion P is not, because the implication ¬P → Q is a premise. It links provability to truth, and no logic supplies it.

Premise-free case. Set Prov := identity. Then Q is ¬P, so the field ¬P → Q holds by reflexivity, and the chain reduces to ¬¬P → P, which is classical logic alone. That case is trivial: it assumes that provability is truth.