module module moderate

`IndisputableMonolith.Holography.SeamTransferCore`

Linear-algebraic core for holographic seam transfer: real eigenvalues of a monodromy, a characteristic anomaly on 2×2 maps, and its identification with the Recognition cost J. Anyone pricing the delivered leg of a seam crossing or discharging B2 uniqueness cites this package. The module is mostly definitions plus elementary matrix identities (trace/det, hyperbolic witness, balanced conjugates).

claimFor a linear map $W$ on the fiber, the predicate that $W$ has real eigenvalue $x$ means some nonzero vector scales by $x$ under one closure (the delivered leg of the seam, with mismatch ratio $x$). The module defines the characteristic anomaly of a $2\times 2$ transfer, proves it equals the cost $J(x)=(x+x^{-1})/2-1$, and supplies a hyperbolic witness matrix with balanced conjugate eigenvalues and controlled determinant.

background

Recognition Science prices closed recognition cycles by the unique cost $J$ forced at T5: $J(x)=(x+x^{-1})/2-1$. Upstream TurnRatioCarrier fixes the B2 reading on the real turn ratio: the per-cycle cost is $C(T)=J(\kappa T/2\pi)$. The seam splits that story into a delivered leg and a required leg; mismatch is a pure scaling ratio.

This module sits in the holography layer and treats the monodromy (or transfer) $W$ as a linear map on the fiber. Having a real eigenvalue $x$ is definitional for the delivered leg: one nonzero vector scales by $x$ under a single closure, with no assumption on the other leg. Companion notions track the characteristic anomaly of a $2\times 2$ transfer, balanced trace/conjugate structure, diagonalizability under balance, and elementary rotation and hyperbolic witnesses.

proof idea

Definition-and-identity module, not a single deep theorem. It introduces the real-eigenvalue predicate, the characteristic anomaly (via det of a shifted map), and a hyperbolic witness matrix. Supporting lemmas are standard $2\times 2$ linear algebra: characteristic polynomial evaluations, trace and determinant identities for balanced conjugates, eigenvalue extraction for the witness, and the key equality that the characteristic anomaly coincides with $J$. Rotation and diagonal-balance equivalences close the local toolkit.

why it matters in Recognition Science

Downstream SeamLedgerDischarge imports this core to type the R1–R4 residue of ConservingSeamPricing in ledger language and to keep B2 (the deficit-free period $\beta=2\pi/\kappa$ is the unique zero of per-cycle seam cost) under a strict weakening of the fourth conjunct. Without a clean delivered-leg eigenvalue and the anomaly$\leftrightarrow J$ bridge, the seam cost cannot be pushed below the anomaly reading while staying honest to the panel’s B2 plan. The module therefore anchors the holographic half of the eight-tick pricing story (T7 octave, T5 $J$) before ledger discharge.

scope and limits

Does not prove uniqueness of the deficit-free period $\beta=2\pi/\kappa$ (that is B2, discharged downstream).
Does not assume or constrain the required leg of the seam, only the delivered scaling.
Does not derive $J$ itself; it only identifies the characteristic anomaly with the already-forced cost.
Does not treat higher-rank transfers or non-real spectra beyond the balanced-conjugate witness.
Does not encode full ConservingSeamPricing; only the linear-algebraic transfer primitives.

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