HyperbolicMismatchClass
plain-language theorem explainer
Marks a real 2×2 matrix and scalar as a positive real eigenvalue other than 1, the hyperbolic (non-elliptic) mismatch leg of seam transfer. Horizon-clock and holography work cite it to type B3's delivered mismatch without asserting period closure. The body is a three-way definitional conjunction: real eigenvalue, positivity, and non-unity.
Claim. For a real $2\times 2$ matrix $W$ and a real number $x$, the hyperbolic mismatch class holds when $x$ is a real eigenvalue of $W$, $x>0$, and $x\neq 1$.
background
HorizonClockRate types only what panel B3 delivers: near-horizon Rindler geometry makes the continued Euclidean angle advance at rate $\kappa$ per unit Euclidean time ($d\theta/d\tau_E=\kappa$). It does not assert the $2\pi$ closure period; that is B2's carrier output (deficit-free Euclidean period and turn-ratio unity).
The physical commitment here is that the delivered mismatch leg sits in the hyperbolic class: a positive real eigenvalue, not $\pm 1$ and not complex. That is the typed reading of the real-eigenvalue predicate from the seam-transfer core. The legacy horizon rate $\kappa=1/R$ is a separate Schwarzschild normalization socket for the Clausius bridge and must not be conflated with this B3 delivery.
proof idea
Definitional abbreviation, not a proved theorem. The predicate is the conjunction of three conditions: the seam-transfer core's real-eigenvalue relation between $W$ and $x$, strict positivity of $x$, and $x\neq 1$. No tactics or upstream lemmas are invoked.
why it matters
Gives the typed physical commitment for the mismatch leg inside the B3 rate-only module. Downstream fence material in the same file (period is B2 output not B3 input; turn-ratio unity at the B2 period; clock-rate bundle silent on period) relies on keeping hyperbolic mismatch separate from period closure and from the legacy $\kappa=1/R$ socket.
In the broader Recognition holography stack this keeps LEG-B honest: rate law only, no smuggling of eight-tick or full-turn structure from T7 into the near-horizon clock. Empty external used-by list so far; the declaration is local typing infrastructure for the fence theorems that follow it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.