Holography Seam Transfer Core

The seam transfer core

In the Recognition Science framework, a ledger (a discrete record of events) keeps two entries for every transaction, a debit and a credit. A seam is a boundary in that record where a cycle of events closes. The seam transfer core is the part of the framework's machine-checked library of formal theorems that asks what it costs, in recognition, for one closure to cross that seam.

The classical mathematics here is a 2 by 2 matrix. The framework models the effect of one closure on the seam's pair of entries as a linear transfer. The core result is that the cost is not a free parameter. If the transfer preserves the ledger's balance (its determinant is 1), and if it scales one entry by a real number x, then the other entry must scale by the reciprocal 1/x. This is a theorem, proved in the library: the product of the eigenvalues of a matrix equals its determinant, so a determinant of 1 forces the second eigenvalue to be the reciprocal of the first. Reciprocity is conservation, not a modeling choice.

From that single fact, the trace of the transfer is forced to be x + 1/x, by the Cayley-Hamilton theorem. The cost, defined as half the trace minus 1, is therefore exactly J(x) = (x + 1/x)/2 - 1, the framework's fundamental cost function. The library proves this equality for any balanced transfer with a real eigenvalue x. The cost function appears nowhere in the assumptions; it emerges from the algebra.

The core also proves a reduction: if every physical seam crossing is priced by such a balanced transfer, then the framework's full census pricing condition follows. This is a theorem in the library. What is not proved is that the physical seam actually delivers such a transfer, that the pair fiber is two-dimensional, or that balance is unimodularity. That remains a model, not a theorem, until derived from the seam ledger itself.

The module also lands a falsifier. For an n-fold retrace of a seam, the two observable surplus measures pair to exactly J(n). The framework predicts the ratio of costs for a triple cover to a double cover is 8/3, not 2. If a physical seam ever prices the triple cover at ratio 2, the trace carrier is dead. That is the signature the framework stakes its claim on.

/-- **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

/-- **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]

/-- **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]

/-- **The reduction theorem (THEOREM).** Any cost functional priced by a balanced
seam transfer satisfies `CensusPricing`: the pricing premise that named J is now
DOWNSTREAM of a premise that does not. Composing with
`TurnRatioCarrier.b2_unique_zero_of_censusPricing`, the deficit-free period
`β = 2π/κ` is the unique zero of any such functional. -/
theorem censusPricing_of_seamTransfer (C : ℝ → ℝ → ℝ)
    (h : SeamTransferPricing C) : TurnRatioCarrier.CensusPricing C := by
  intro kappa T hk hT
  obtain ⟨W, hdet, heig, hC⟩ := h kappa T hk hT
  rw [hC]
  exact charAnomaly_eq_J hdet (TurnRatioCarrier.turnRatio_pos hk hT) heig

/-- **The trace-carrier signature: `J(3)/J(2) = 8/3` (THEOREM).** -/
theorem cover_cost_ratio_eq : Cost.Jcost 3 / Cost.Jcost 2 = 8 / 3 := by
  rw [Jcost_two, Jcost_three]
  norm_num

What this page does not claim

The physical seam is not proved to deliver a balanced transfer. The pair fiber is not proved to be two-dimensional over the reals. The framework does not derive the fine-structure constant from this module.

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: