module module moderate

`IndisputableMonolith.Holography.SeamTransferCore`

Core linear-algebra layer for seam transfer on the holographic boundary: real eigenvalues of a closure map, the characteristic anomaly of a 2x2 transfer, and its identification with the J-cost. Supplies balanced (trace-zero, det-one) witnesses, a hyperbolic witness with explicit spectrum, and a rotation form. Cited by anyone pricing a seam cycle or discharging ConservingSeamPricing. Mostly definitional identities and short matrix calculations.

claimFor a linear closure $W$ on a fiber, $W$ has real eigenvalue $x$ when some nonzero vector scales by $x$ under one step (the delivered mismatch ratio). The characteristic anomaly of a $2\times 2$ transfer is the scalar that measures det-trace imbalance; on balanced matrices it equals $J(x)=(x+x^{-1})/2-1$. A hyperbolic witness realizes spectrum $\{x,x^{-1}\}$ with $\det=1$; a rotation form covers the oscillatory case.

background

Recognition holography prices the continued eight-tick cycle on the real turn ratio. Upstream TurnRatioCarrier fixes the per-cycle cost as $C(T)=J(\kappa T/2\pi)$ with the T5 cost $J(x)=(x+x^{-1})/2-1$ from Cost.Jcost. The seam is the interface where a required leg and a delivered leg meet; mismatch is a scaling ratio, not an additive deficit.

This module isolates the linear-algebra core of that transfer. HasRealEigen packages the delivered-leg statement: some nonzero fiber vector scales by a real $x$ under one closure, with no assumption on the other leg. Balanced matrices (trace zero in the appropriate normalization, conjugate spectrum) and a hyperbolic witness supply concrete carriers whose characteristic anomaly collapses to $J$. A rotation companion covers the compact/oscillatory branch of the same $2\times 2$ picture.

proof idea

Definition-and-identity module, not a long derivation. HasRealEigen is a Prop packaging existence of a real eigenpair. Characteristic anomaly is defined via det and scalar-multiple-of-identity comparison; eigen_char and det_sub_smul_one relate the char poly to that scalar. Balanced_trace and balanced_conjugate pin the SL-like normal form; charAnomaly_eq_J is the algebraic reduction that the anomaly equals $J$ on that form. HyperbolicWitness builds an explicit matrix with det one and real spectrum ${x,x^{-1}}$; companion lemmas record det and eigen facts. Diag_balanced_iff and rotation close the classification for the diagonal and circular cases. Proofs are short matrix algebra over Mathlib.

why it matters in Recognition Science

SeamLedgerDischarge imports this module to type the R1–R4 residue of ConservingSeamPricing in ledger language and to keep B2 (uniqueness of the deficit-free period $\beta=2\pi/\kappa$ as the zero of per-cycle seam cost) under a weakened fourth conjunct. Without a clean identification of the transfer anomaly with $J$, the turn-ratio pricing $C(T)=J(\kappa T/2\pi)$ cannot be read off the seam map. The module therefore sits between Cost/TurnRatioCarrier and the holography discharge stack: it turns the delivered-leg scaling story into the same $J$ that forces the eight-tick octave cost structure (T5–T7 landmarks). Parent consumers are the ConservingSeamPricing conjuncts and the B2 uniqueness argument in SeamLedgerDischarge.

scope and limits

Does not prove uniqueness of the deficit-free period $\beta=2\pi/\kappa$ (that is B2 downstream).
Does not assume or construct the required leg; only the delivered real-eigenvalue leg.
Does not derive $J$-uniqueness from the Recognition Composition Law; it only matches the anomaly to $J$.
Does not treat higher-rank or infinite-dimensional fiber maps beyond the $2\times 2$ witness calculus.
Does not discharge ConservingSeamPricing residues R1–R4; it only supplies the transfer core.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Holography.SeamLedgerDischarge module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Holography.TurnRatioCarrier module_import

declarations in this module (35)

def HasRealEigen L79
def charAnomaly L84
lemma det_sub_smul_one L89
lemma eigen_char L99
theorem balanced_trace L112
theorem balanced_conjugate L125
theorem charAnomaly_eq_J L143
def hyperbolicWitness L155
theorem hyperbolicWitness_det L158
theorem hyperbolicWitness_eigen L164
theorem diag_balanced_iff L178
def rotation L187
theorem rotation_det L190
theorem charAnomaly_rotation L200
theorem elliptic_no_real_mismatch L210
def pairForm L237
lemma pairForm_map L241
theorem preserves_pairForm_iff_det_one L253
theorem trace_inv_eq_of_det_one L271
def SeamTransferPricing L292
theorem censusPricing_of_seamTransfer L304
theorem seamTransferPricing_turnRatioCost L314
theorem b2_unique_zero_of_seamTransfer L327
def ConservingSeamPricing L342
theorem seamTransferPricing_of_conserving L350
theorem b2_unique_zero_of_conserving L360
theorem Jcost_pairing L372
theorem surplus_pairing_eq_J L381
theorem Jcost_two L388
theorem Jcost_three L393
theorem cover_cost_ratio_eq L398
theorem pricing_discriminated L407
theorem witnessWalk3_census L420
structure SeamTransferCoreCert L437
theorem seamTransferCoreCert L457