Encyclopedia Holography Holography Seam Transfer Core Seam Transfer Pricing Of Conserving

ARTICLE 5 claims 5 theorems

Holography Seam Transfer Core Seam Transfer Pricing Of Conserving

A single algebraic condition, that a seam transfer preserves a two-entry ledger, is enough to force the framework's cost function; the physical seam itself remains a model, not a theorem.

Verify this page

Conservation forces the cost

The declaration seamTransferPricing_of_conserving is a theorem in the framework's machine-checked library of formal theorems. It states that if a pricing rule for a seam crossing is conserving, meaning it preserves a two-dimensional area form on a pair of entries, then that rule automatically satisfies the framework's SeamTransferPricing condition. The condition requires that the cost of a crossing equals half the trace of a 2x2 matrix, minus one, where the matrix has determinant one and an eigenvalue equal to the turn ratio of the crossing.

The proof is a short chain of linear algebra. A conserving transfer has determinant one, because preserving the area form is equivalent to having unit determinant. If such a transfer has a real eigenvalue x, then its other eigenvalue must be x⁻¹, since the product of eigenvalues is the determinant. The trace, the sum of eigenvalues, is therefore x + x⁻¹. The cost, defined as half the trace minus one, becomes (x + x⁻¹)/2 - 1, which is exactly the framework's cost function J(x). The theorem shows J appears nowhere in the assumptions; it emerges from conservation and one eigenvalue.

The declaration also reduces a stronger pricing premise to a weaker one. If a physical seam delivers such a balanced transfer, then the full CensusPricing condition follows. This reduction is significant because the pricing premise that names J is replaced by checkable structural facts: a two-dimensional pair fiber, a unit determinant, a delivered-leg eigenvalue, and a trace reading. None of these name the answer.

What the theorem does not claim is that the physical seam actually delivers such a transfer. The residue that the pair fiber is two-dimensional over the reals, that one closure acts linearly with the delivered leg scaling by the turn ratio, and that double-entry balance is unimodularity, is typed as SeamTransferPricing and remains a MODEL. The theorem proves per-closure matrix algebra and the reduction; it does not prove the physical seam obeys the model. That link stays open.

THEOREM seamTransferPricing_of_conserving · IndisputableMonolith/Holography/SeamTransferCore.lean
seamTransferPricing_of_conserving · IndisputableMonolith/Holography/SeamTransferCore.lean:349 
/-- Conservation pricing is transfer pricing (`Sp(2) = SL(2)` applied). -/
theorem seamTransferPricing_of_conserving (C : ℝ → ℝ → ℝ)
    (h : ConservingSeamPricing C) : SeamTransferPricing C := by
  intro kappa T hk hT
  obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
  exact ⟨W, (preserves_pairForm_iff_det_one W).mp hcons, heig, hC⟩
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 · 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
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]
THEOREM censusPricing_of_seamTransfer · IndisputableMonolith/Holography/SeamTransferCore.lean
censusPricing_of_seamTransfer · IndisputableMonolith/Holography/SeamTransferCore.lean:299 
/-- **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

What this page does not claim

The physical seam delivers the balanced transfer; that the pair fiber is two-dimensional, the closure acts linearly, and double-entry balance is unimodularity remains a MODEL. The theorem proves the full flow classification of seam dynamics, which is Phase A in a sibling module. The elliptic class can carry a genuine mismatch ratio other than one; the theorem proves it cannot.

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