Holography Seam Transfer Core Elliptic No Real Mismatch

The elliptic dead end

A rotation matrix is the algebraic picture of turning something without stretching or shrinking it. In the plane, a rotation by angle θ sends a vector to another vector of the same length, swung around the origin. The matrix that does this has determinant 1 and, unless θ is a multiple of π, no real eigenvalue other than ±1: no nonzero vector is mapped to a scalar multiple of itself. The Recognition Science declaration elliptic_no_real_mismatch states exactly this fact as a theorem: if a rotation matrix has a real eigenvalue x, then x is either 1 or −1.

The point of the theorem is negative. In the framework's model of a seam crossing, a mismatch ratio x > 0, x ≠ 1 would have to appear as a real eigenvalue of a 2×2 transfer matrix. A rotation matrix cannot supply that eigenvalue. So the entire elliptic class of transfers, the rotations, is provably unable to carry a genuine mismatch. The earlier dead end in the framework's development was not bad luck; it was the wrong conjugacy class, and the theorem shows why.

What the theorem does not do is say that a physical seam crossing actually delivers such a transfer. That the pair fiber is 2-dimensional over the reals, that one closure acts on it linearly, and that double-entry balance is unimodularity, all remain modeling assumptions, not proved facts. The theorem is a piece of matrix algebra with a precise scope: it rules out rotations as carriers of mismatch, and it does not rule in anything else.

/-- **The elliptic class cannot carry a mismatch (THEOREM).** A rotation admits no
real eigenvalue besides ±1: `(x − cos θ)² = cos²θ − 1 ≤ 0` forces `x = cos θ = ±1`.
So no genuine ratio `x > 0, x ≠ 1` lives on the elliptic branch; pricing mismatches
there was structurally impossible, not merely unlucky. -/
theorem elliptic_no_real_mismatch {θ x : ℝ}
    (h : HasRealEigen (rotation θ) x) : x = 1 ∨ x = -1 := by
  have hchar := eigen_char h
  rw [rotation_det] at hchar
  have htr : (rotation θ).trace = 2 * Real.cos θ := by
    unfold rotation
    rw [Matrix.trace_fin_two_of]
    ring
  rw [htr] at hchar
  have hsq : (x - Real.cos θ) ^ 2 = Real.cos θ ^ 2 - 1 := by nlinarith
  have hcos1 : Real.cos θ ^ 2 ≤ 1 := by
    nlinarith [Real.neg_one_le_cos θ, Real.cos_le_one θ]
  have hz1 : (x - Real.cos θ) ^ 2 = 0 := by
    nlinarith [sq_nonneg (x - Real.cos θ)]
  have hz2 : Real.cos θ ^ 2 = 1 := by nlinarith [sq_nonneg (x - Real.cos θ)]
  have hxcos : x = Real.cos θ := by nlinarith [hz1]
  have hfac : (Real.cos θ - 1) * (Real.cos θ + 1) = 0 := by nlinarith [hz2]
  rcases mul_eq_zero.mp hfac with h1 | h1
  · left; rw [hxcos]; linarith
  · right; rw [hxcos]; linarith

What this page does not claim

The physical seam crossing delivers a transfer of the required kind. The pair fiber is 2-dimensional over the reals. Double-entry balance is unimodularity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/SeamTransferCore.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: