Holography Seam Transfer Core Seam Transfer Pricing Turn Ratio Cost

A pricing rule from a transfer matrix

In the Recognition Science framework, a ledger, a discrete record of events, can carry a cost for each transition. The declaration seamTransferPricing_turnRatioCost is a theorem in the framework's machine-checked library of formal theorems. It proves that a specific pricing rule, one based on a turn ratio, satisfies a more general structural condition called SeamTransferPricing.

The classical mathematics here is a 2 by 2 matrix, a square array of four numbers. The theorem concerns a matrix whose determinant, a number measuring how it scales areas, equals 1. If such a matrix has a real eigenvalue, a number that the matrix merely scales along some direction, and that eigenvalue is the turn ratio, then the matrix's trace, the sum of its diagonal entries, is forced. The theorem proves that half the trace minus one equals the cost function J(x) = (x + 1/x)/2 - 1. Reciprocity, the appearance of 1/x, is not assumed; it is derived from the determinant being 1, which the framework interprets as double-entry balance, a conservation law.

The theorem's role is reduction. It shows that a pricing premise which names the answer, J, can be replaced by a premise that does not: a 2 by 2 pair fiber, a unit determinant, a delivered-leg eigenvalue, and a trace reading. Each of these is a checkable structural fact. The theorem also proves that a rotation matrix, one that spins vectors without stretching them, cannot carry a genuine mismatch ratio other than 1. That class is provably dead for this purpose.

What the theorem does not claim is that the physical seam actually delivers such a transfer. That the pair fiber is two-dimensional, that one closure acts linearly, and that double-entry balance is unimodularity remain a model, not a derived result. The theorem also provides a numeric falsifier: the ratio of costs at the triple cover, J(3)/J(2), is 8/3, not 2. If a physical seam ever prices that triple cover at ratio 2, the trace carrier is dead.

/-- Non-vacuity of the premise: the turn-ratio cost itself is transfer-priced (by
the hyperbolic witness). Existence check only; the physical identification of the
SEAM's transfer stays open. -/
theorem seamTransferPricing_turnRatioCost :
    SeamTransferPricing TurnRatioCarrier.turnRatioCost := by
  intro kappa T hk hT
  have hx : 0 < TurnRatioCarrier.turnRatio kappa T :=
    TurnRatioCarrier.turnRatio_pos hk hT
  refine ⟨hyperbolicWitness (TurnRatioCarrier.turnRatio kappa T),
    hyperbolicWitness_det _ (ne_of_gt hx), hyperbolicWitness_eigen _, ?_⟩
  rw [charAnomaly_eq_J (hyperbolicWitness_det _ (ne_of_gt hx)) hx
    (hyperbolicWitness_eigen _)]
  rfl

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

/-- **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 delivers such a transfer; that the pair fiber is 2-dimensional, that one closure acts linearly, and that double-entry balance is unimodularity remain MODEL. The flow half of the program, the Fricke to d'Alembert to T5 classification, is proved in this module; it lives in a sibling module. Any consumer of this theorem is unconditional; consumers remain FORCED-CONDITIONAL because the weakest link sets the tag.

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: