IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D

declarations in this module (20)

• structure DualEntryStrainState L66
• abbrev discreteCarrier L111
• theorem recognitionLedger_cost_ext L160
• def enrichedWitness L193
• theorem enrichedWitness_strain L212
• theorem enrichedWitness_extract_zero L228
• def enrichedWitnessLedger L233
• theorem enrichedWitnessLedger_phi_abs_le_one L239
• theorem enrichedWitness_eq_ofLedger L255
• theorem enrichedWitness_toBare L263
• theorem toBare_not_injective L303
• theorem bare_factorable_is_swap_even L315
• def RecoversExtractFromBare L323
• theorem extract_not_bare_factorable L329
• def TypedResidual_signed_source_enrichment_schema L345
• theorem typedResidual_signed_source_enrichment_schema_closed L353
• theorem TypedResidual_signed_source_enrichment_schema_closed L358
• structure RecognitionDualEntryEnrichment4DStatus L364
• def recognitionDualEntryEnrichment4DStatus L369
• theorem recognitionDualEntryEnrichment4DStatus_flags L375