Holography Seam Transfer Core Census Pricing Of Seam Transfer

The reduction theorem

In the Recognition Science framework, a seam is a boundary where two cycles of a ledger meet, and a transfer is a linear map that one cycle induces on the other's state. The theorem censusPricing_of_seamTransfer states a reduction: if the per-cycle cost of a seam crossing is the character anomaly of some balanced transfer, then the framework's CensusPricing rule holds. The character anomaly is half the trace of the transfer matrix minus one, and a balanced transfer is one whose determinant equals one, meaning it preserves a certain area form. The theorem proves that this structural condition is enough to force the pricing rule, without the rule itself appearing in the premise.

The proof rests on two algebraic facts, both proved in the machine-checked library. First, if a balanced 2x2 transfer has a real eigenvalue x, then it also has the reciprocal eigenvalue 1/x, because the product of eigenvalues equals the determinant, which is one. Second, the trace of such a transfer is x + 1/x, by the characteristic polynomial. Substituting these into the character anomaly gives (x + 1/x)/2 - 1, which is exactly the framework's cost function J(x). The theorem shows that J emerges from the algebra of a balanced transfer, rather than being assumed as an input.

The theorem also carries a falsifier. The framework's cost function predicts that the ratio of costs for a triple cover versus 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. The library includes a machine-checked witness for the triple retrace, confirming the census counts and the cost ratio.

What the theorem does not claim is that a physical seam actually delivers such a transfer. That the pair fiber is two-dimensional, that a closure acts linearly with the delivered leg scaling by the turn ratio, and that double-entry balance is unimodularity, all remain MODEL assumptions, not derived facts. The reduction is conditional on those structural premises holding.

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

/-- **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 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 theorem does not prove that a physical seam delivers a balanced transfer with the required eigenvalue. The theorem does not derive the structural premises of SeamTransferPricing from the ledger itself. The theorem does not claim that the elliptic class can carry a genuine mismatch ratio other than one.

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: