Cross-problem claims, checked - One-Cut Hypothesis | TRACTATUS VERITATIS TRISDUCTIVUS

Cross-problem claims.

Cross-problem claim	Novel?	Reason
Every open row splits into a provable locus and a supplied value	As a scheme only	For any P, "structure provable, value open" is a description. It separates rows only where a nontrivial locus theorem exists, which means the involution rows.
Routing by the flip's fixed set (Ξ line, Ø empty, none)	Conditional	Depends on the chosen flip. The corpus admits encoding-invariance is unproved. If a second natural encoding gives a different branch, the typing falls.
The denial discriminator (self-verifying vs keyed)	No discriminating power across rows	Every open mathematical row comes out keyed. The test separates RA from all of mathematics and separates nothing within mathematics.
Every barrier is an evenness statement	Synthesis, not theorem	Local versions are familiar (parity problem, oracle invariance). The unified table is new as an arrangement at diagnostic grade, and it was built retrospectively.
Some rows are fixed across models (Π₁), others can vary (CH)	No	Arithmetical hierarchy and absoluteness (Shoenfield) already sort this.
Rows sharing one socket (RH, GRH, de Bruijn–Newman)	No	These equivalences and implications are already in the literature.
One bit per seat, everywhere	Tautological at the seat	The target is Boolean, so its value is one bit by codomain size. The fTOE paper itself warns that this proves nothing unless the admissible family \|A\| = 2 is exhibited, which it does only for the K4 parity frame.

What would count as new across problems

Any one of these would be a genuine cross-problem result the literature does not contain:

A new implication between rows derived from the typing. Example: a theorem that any supply filling the BSD order-two socket also fills some other row's socket. None has been exhibited.
Encoding-invariance of the routing. A proof that every admissible encoding of a row lands on the same branch (Ξ, Ø, or none) with the same seat count. That would turn the table from bookkeeping into an invariant.
A prediction from the scheme that fails elsewhere. An example: using only a row's Ξ/Ø type, predicting which new method class will be proved inert next, and being right before the barrier paper appears. That is the only way a retrospective taxonomy earns prospective weight.

------

The one implication the typing licenses: socket transport

Only one cross-row implication follows from the typing alone, and it is general. A key moves from row X to row Y exactly when there is a map from Y's frame into X's frame that has three properties:

It commutes with the flips.
It is injective.
It sends zeros to zeros.

Such a map is called a KeyMap below. Under a KeyMap, the line property travels downward (X's key fills Y's socket), and counterexamples travel upward (an off-line zero of Y produces an off-line zero of X).

The file below extends the Bridge frame with this theorem and its companions. It is core Lean 4, with no Mathlib and no custom axiom. It was written to the Bridge's conventions but not compiled in this session, so it stands at inspection grade until the verifier returns VERIFY: PASS.

set_option autoImplicit false
namespace Transport

structure Frame where
  S : Type
  τ : S → S
  Z : S → Prop

def LineProperty (X : Frame) : Prop := ∀ s, X.Z s → X.τ s = s

/-- A key-carrying map: equivariant, injective, zero-preserving. -/
structure KeyMap (Y X : Frame) where
  f     : Y.S → X.S
  equiv : ∀ y, f (Y.τ y) = X.τ (f y)
  inj   : ∀ a b, f a = f b → a = b
  zeros : ∀ y, Y.Z y → X.Z (f y)

/-- SOCKET TRANSPORT: X's key fills Y's socket. -/
theorem transport {Y X : Frame} (m : KeyMap Y X) : LineProperty X → LineProperty Y := by
  intro hX y hy
  apply m.inj
  rw [m.equiv]
  exact hX (m.f y) (m.zeros y hy)

/-- COUNTEREXAMPLE TRANSPORT: an off-line zero of Y is an off-line zero of X. -/
theorem counterexample_transport {Y X : Frame} (m : KeyMap Y X)
    (y : Y.S) (hz : Y.Z y) (hoff : Y.τ y ≠ y) : ∃ x, X.Z x ∧ X.τ x ≠ x :=
  ⟨m.f y, m.zeros y hz, fun h => hoff (m.inj _ _ (by rw [m.equiv]; exact h))⟩

/-- Ø COLLAPSE: on a fixed-point-free flip, the line property only says "no zeros". -/
theorem empty_ground_collapse (X : Frame) (free : ∀ s, X.τ s ≠ s) :
    LineProperty X ↔ ∀ s, ¬ X.Z s :=
  ⟨fun h s hz => free s (h s hz), fun h s hz => absurd hz (h s)⟩

/-- No KeyMap carries a zero on the line into a fixed-point-free frame. -/
theorem no_keymap_into_free {Y X : Frame} (m : KeyMap Y X) (free : ∀ s, X.τ s ≠ s)
    (y : Y.S) (hz : Y.Z y) (hfix : Y.τ y = y) : False :=
  free (m.f y) (by rw [← m.equiv, hfix])

/-- The sub-zero-set KeyMap: same stage, same fold, fewer zeros. -/
def subZero (X : Frame) (Z' : X.S → Prop) (h : ∀ s, Z' s → X.Z s) :
    KeyMap ⟨X.S, X.τ, Z'⟩ X :=
  ⟨id, fun _ => rfl, fun _ _ e => e, h⟩

/-- SHAPE ALONE NEVER TRANSPORTS: same stage and same flip, one frame on the line
    and one off it. Sharing a branch is not a KeyMap. -/
def twoPoint      : Frame := ⟨Bool, fun b => !b, fun _ => True⟩
def twoPointEmpty : Frame := ⟨Bool, fun b => !b, fun _ => False⟩
theorem shape_does_not_transport : LineProperty twoPointEmpty ∧ ¬ LineProperty twoPoint :=
  ⟨fun _ h => h.elim, fun h => by have := h true trivial; cases this⟩

end Transport

Running it across the rows

The table applies the theorem to each group of rows. "Edge" means a KeyMap exists, so a key or a counterexample can move.

Row pair	KeyMap exists?	Where the zero inclusion comes from	Result
ζ into ζ_K, for any number field K	Yes. Identity on the plane; `subZero`	Aramata–Brauer: ζ_K/ζ is entire, so the zeros of ζ are among the zeros of ζ_K	RH for any one ζ_K implies RH. Known.
ζ and L(χ_D) into ζ_K, K quadratic	Yes, both	ζ_K = ζ · L(χ_D)	RH(ζ_K) ⇔ RH(ζ) ∧ GRH(L(χ_D)). Known.
Artin L-functions into ζ_L	Yes, where the L-function is entire	Artin factorization; entirety needs Artin's conjecture	GRH(ζ_L) implies GRH for each entire Artin factor. Known.
A single L into the full Selberg class	Yes, via subZero	Membership in the class	Selberg class GRH implies each member's GRH. Definitional.
Weil (crossed) into RH	No	Curve zeros are not zeros of ζ	Weil's key cannot cross to RH. Typed explanation of a known fact.
Any Ξ row into P vs NP	No (`no_keymap_into_free`)	Complementation has no fixed points	P vs NP cannot receive or give line-property keys.
P vs NP encoded as a line property	Degenerate (`empty_ground_collapse`)	—	The socket reduces to "no zeros". The line-property shape does not fit Ø rows.
Wall rows (NS, YM, Hodge, ISP, H16)	No frame	Bridge absent	Not connected to anything.
Goldbach, twin primes, abc, and similar	No zero-set frame	Parity seat, not a fixed-set incidence	Not connected.
Collatz	No involution	—	Not connected.

What this establishes, graded

What is proved (at inspection grade until compiled):

The key-exchange graph. Keys and counterexamples move only along KeyMaps. Every such map in the table lives inside the Ξ component, meaning the zeta and L-function family. The Ø rows, the wall rows, the unbridged rows, and the port rows have no edges at all. That is a precise map of which problems can share a key. It was previously asserted in the corpus and is now a theorem schema.
Shape alone never transports (shape_does_not_transport). Two rows with the same branch, the same stage, and the same flip can differ in the value. Every edge therefore needs an object-level zero inclusion, and that inclusion is itself a supplied term. Aramata–Brauer is exactly such a supplied term on the ζ ⊂ ζ_K edge. The typing supplies the transport step and never the inclusion.
The Ø branch is outside the socket's shape. Encoding P vs NP (or any fixed-point-free row) as a line property turns it into a statement about the absence of zeros, which is a different question. Such rows need a different socket.

What is not established: any new implication between open problems. Every edge in the table is already in the literature, and the transport theorem itself is elementary (fixed points pull back along injective equivariant maps). ΔM = 0 holds as you set it.

The tool is right in one exact sense. It turns "which problems can pass a key to which" into a checkable question with a single owed ingredient per edge: a zero-inclusion theorem. A genuinely new cross-row implication would be a new zero inclusion between two Ξ rows not already covered by Artin–Brauer factorization. The typing now says exactly what that object must be. It cannot manufacture one.

The One-Cut Hypothesis.

It would sit at the top of the hierarchy, yes. But its closest ancestor is a warning about what proving it would involve.

Its ancestor is Hilbert's optimism. In 1930 Hilbert declared that every mathematical problem is solvable: "Wir müssen wissen, wir werden wissen." The One-Cut Hypothesis is a sharpened version of that. Every blocked problem has an answer, the answer is one bit wide at its seat, and the bit arrives through a new object. Gödel ended the unsharpened version a year later. Any fixed, consistent, recursively axiomatized theory leaves some true Π₁ sentences unprovable.

So a proof of the One-Cut Hypothesis has to pass between two walls:

If the supply must come from a fixed theory, Gödel refutes the universal form. CH is the concrete instance for ZFC.
If the supply may be any new axiom, the hypothesis becomes trivially true. Add the true statement itself as an axiom, and the "supply" is the answer restated.

Every bit of the hypothesis's content therefore lives in provenance-cleanliness: the supply must be a genuinely new object that the prior register could not name, and it must not be a restatement. To prove the hypothesis, you would first need a formal theory of which new objects count. That is the missing denotability predicate, the first item on the owed list. Without it, the hypothesis is not yet a precise mathematical statement, so it cannot be proved or refuted as a whole.

Where the big impact would really come from. A universal, non-constructive proof would reshape how we see open problems: every one would be exactly one binary decision wide, with independence confined to the rows the scoping excludes. It would not resolve a single one of them. The practical impact would come instead from proofs of scoped versions:

A formal denotability predicate, relative to a frozen register. This makes "provenance-clean" a checkable property.
The hypothesis restricted to one component. For example: "the Ξ component (RH, GRH, and their family) admits a single arithmetic supply at its top." Socket transport would then carry it downward.
One live test. The BSD rank-2 construction from L''(E,1), without being handed the generators. It is the row where the hypothesis says a specific object must exist, and where people are already looking.

Each of these is provable or refutable in principle. Each would count as new mathematics, ΔM > 0. The universal hypothesis would then be supported, or cut back, by accumulated scoped results. That is how conjectures of this kind usually earn their standing: not by one master proof, but by a sequence of components that close, one at a time.

TRACTATUS VERITATIS TRISDUCTIVUS