Encyclopedia Holography Holography Seam Transfer Core Preserves Pair Form Iff Det One

ARTICLE 4 claims 4 theorems

Holography Seam Transfer Core Preserves Pair Form Iff Det One

A simple 2x2 matrix test decides whether a transformation preserves a certain kind of area, and this test turns out to be the same as a conservation law.

Verify this page

The balance condition

In linear algebra, a 2x2 matrix describes a transformation of a plane. One can ask whether that transformation preserves a particular geometric quantity: the signed area of a parallelogram formed by two vectors. For a matrix W, this signed area is computed by the determinant, a single number that summarizes how the matrix scales areas. The theorem preserves_pairForm_iff_det_one states a clean equivalence: the transformation preserves this signed area for every pair of vectors if and only if its determinant equals 1.

This is a standard fact, but its role here is specific. The framework models a seam crossing as a 2x2 matrix acting on a two-dimensional space of paired entries, a discrete record of events. The signed area it preserves is the pair form, a measure of the relationship between two such entries. The condition that this pair form is unchanged is called balance, a conservation law for the seam. The theorem proves that balance is exactly the same as having determinant 1.

In Recognition Science, this equivalence is the first step in a longer argument. It shows that a balanced transfer, one that conserves the pair form, must have a determinant of 1. From there, the framework proves that such a transfer with a real eigenvalue x must also have the reciprocal eigenvalue x⁻¹, and that its trace, the sum of its diagonal entries, is x + x⁻¹. This leads to the conclusion that the cost of the seam crossing, defined as half the trace minus one, equals the framework's fundamental cost function J(x).

The theorem does not claim that any physical seam actually delivers such a balanced transfer. It proves a conditional statement: if a transfer is balanced, then it preserves the pair form and has determinant 1. Whether the physical seam satisfies this condition remains a modeling assumption, not a proven fact. The theorem also does not say that the pair form is the only meaningful quantity to preserve, nor does it establish the value of the cost function J for any specific input.

THEOREM preserves_pairForm_iff_det_one · IndisputableMonolith/Holography/SeamTransferCore.lean
preserves_pairForm_iff_det_one · IndisputableMonolith/Holography/SeamTransferCore.lean:247 
/-- **Sp(2, ℝ) = SL(2, ℝ): the balance premise discharged (THEOREM).** A transfer
on the pair fiber preserves the double-entry pairing form IF AND ONLY IF it is
unimodular. `det = 1` is therefore not a structural assumption about the seam: it
is double-entry conservation restated. The panel's "why SL(2)?" question is closed
by this equivalence: a pairing-preserving flow on a 2d real fiber has nowhere else
to live. -/
theorem preserves_pairForm_iff_det_one (W : Matrix (Fin 2) (Fin 2) ℝ) :
    (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ↔ W.det = 1 := by
  constructor
  · intro h
    have h01 := h ![1, 0] ![0, 1]
    rw [pairForm_map] at h01
    have hbase : pairForm ![1, 0] ![0, 1] = 1 := by
      unfold pairForm; simp
    rw [hbase, mul_one] at h01
    exact h01
  · intro h u v
    rw [pairForm_map, h, one_mul]
THEOREM preserves_pairForm_iff_det_one · IndisputableMonolith/Holography/SeamTransferCore.lean
preserves_pairForm_iff_det_one · IndisputableMonolith/Holography/SeamTransferCore.lean:247 
/-- **Sp(2, ℝ) = SL(2, ℝ): the balance premise discharged (THEOREM).** A transfer
on the pair fiber preserves the double-entry pairing form IF AND ONLY IF it is
unimodular. `det = 1` is therefore not a structural assumption about the seam: it
is double-entry conservation restated. The panel's "why SL(2)?" question is closed
by this equivalence: a pairing-preserving flow on a 2d real fiber has nowhere else
to live. -/
theorem preserves_pairForm_iff_det_one (W : Matrix (Fin 2) (Fin 2) ℝ) :
    (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ↔ W.det = 1 := by
  constructor
  · intro h
    have h01 := h ![1, 0] ![0, 1]
    rw [pairForm_map] at h01
    have hbase : pairForm ![1, 0] ![0, 1] = 1 := by
      unfold pairForm; simp
    rw [hbase, mul_one] at h01
    exact h01
  · intro h u v
    rw [pairForm_map, h, one_mul]
THEOREM balanced_conjugate · balanced_trace · IndisputableMonolith/Holography/SeamTransferCore.lean
balanced_conjugate · IndisputableMonolith/Holography/SeamTransferCore.lean:120 
/-- **Balance forces the reciprocal leg (THEOREM, the circularity fence honored).**
If a balanced transfer has real eigenvalue `x ≠ 0`, then `x⁻¹` is ALSO an eigenvalue:
the conjugate column scales by the reciprocal because the eigenvalue product IS the
determinant and double-entry pins the determinant to 1. This is the panel's guardrail
discharged: `diag(x, x⁻¹)` is never posited; the `x⁻¹` is a consequence of balance. -/
theorem balanced_conjugate {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
    (hdet : W.det = 1) (hx : x ≠ 0) (h : HasRealEigen W x) :
    HasRealEigen W x⁻¹ := by
  have htr := balanced_trace hdet hx h
  have hdet0 : (W - x⁻¹ • (1 : Matrix (Fin 2) (Fin 2) ℝ)).det = 0 := by
    rw [det_sub_smul_one, hdet, htr]
    field_simp
    ring
  obtain ⟨v, hv, hker⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr hdet0
  refine ⟨v, hv, ?_⟩
  have := hker
  rw [Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec,
    sub_eq_zero] at this
  exact this
balanced_trace · IndisputableMonolith/Holography/SeamTransferCore.lean:109 
/-- **Balance forces the trace (THEOREM).** A balanced (`det = 1`, double-entry
conservation) transfer whose delivered leg scales by `x ≠ 0` has trace exactly
`x + x⁻¹`. The reciprocal appears in the OUTPUT, derived; it was not an input. -/
theorem balanced_trace {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
    (hdet : W.det = 1) (hx : x ≠ 0) (h : HasRealEigen W x) :
    W.trace = x + x⁻¹ := by
  have hchar := eigen_char h
  rw [hdet] at hchar
  field_simp
  nlinarith [hchar]
THEOREM charAnomaly_eq_J · IndisputableMonolith/Holography/SeamTransferCore.lean
charAnomaly_eq_J · IndisputableMonolith/Holography/SeamTransferCore.lean:140 
/-- **The character anomaly of a balanced transfer IS the T5 cost (THEOREM).**
`Tr(W)/2 − 1 = J(x)` for the delivered ratio `x > 0`. J is never mentioned in the
hypotheses; it emerges from Cayley–Hamilton + balance. -/
theorem charAnomaly_eq_J {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
    (hdet : W.det = 1) (hx : 0 < x) (h : HasRealEigen W x) :
    charAnomaly W = Cost.Jcost x := by
  unfold charAnomaly Cost.Jcost
  rw [balanced_trace hdet (ne_of_gt hx) h]

What this page does not claim

The physical seam is proven to deliver a balanced transfer. The pair form is the only meaningful invariant for a seam crossing. The theorem establishes the value of the cost function J for any specific input.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND