module module

`IndisputableMonolith.Holography.SeamTransferCore`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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