IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D

declarations in this module (39)

• abbrev Mat4 L65
• abbrev Wave4 L66
• abbrev exactFlatCrossTermFold L67
• theorem frobeniusNormSq_preflight_eq_identity L69
• theorem waveNormSq_preflight_eq_identity L74
• abbrev edge_tt_decomposition L81
• abbrev S_RS_converges_EH_4d L84
• theorem edge_tt_decomposition_closed L89
• theorem edge_tt_polarization_witnesses L93
• theorem edge_tt_gauge_decoy_not_transverse L98
• theorem srs_converges_eh_4d_requires_both_gates L102
• theorem discrete_bookkeeping_times_unitF_eq_EH L106
• theorem adversarial_decoys_still_hold L111
• structure SRSConvergesEH4DStatus L125
• def srsConvergesEH4DStatus L132
• theorem srsConvergesEH4DStatus_flags L139
• theorem srs_closer_closed L147
• def TypedResidual_fold_eq_midpointBloch L154
• def TypedResidual_midpointBloch_symbolZero L158
• def TypedResidual_m2_rayleigh_eq_algebraic_face L161
• def TypedResidual_discrete_torus_family_bridge L173
• theorem typedResidual_midpointBloch_symbolZero_closed L185
• theorem typedResidual_m2_rayleigh_eq_algebraic_face_closed L191
• theorem typedResidual_discrete_torus_family_bridge L196
• theorem typedResidual_discrete_torus_family_bridge_closed L200
• theorem typedResidual_discrete_torus_family_bridge_of_symbolZero L204
• theorem continuumSymbolIs_of_discrete_torus_bridge L211
• def TypedResidual_m2_optionC_faces L220
• theorem typedResidual_m2_optionC_faces L233
• theorem continuumEHTarget_of_bridge_and_m2_faces L268
• theorem continuumGaugeZeroTarget_of_bridge_and_m2_faces L277
• theorem srs_converges_eh_4d_of_m2_optionC_faces L288
• theorem TypedResidual_m2_optionC_faces_closed L294
• theorem S_RS_converges_EH_4d_closed L298
• def TypedResidual_continuum_discreteExact_rebind L304
• def GeometricTendstoResidualOpen L313
• theorem discrete_torus_bridge_closed_srs_closed L321
• theorem geometric_tendsto_residuals_named_srs_closed L331
• theorem decoy_finiteN_tt_norm_ne_exact_EH_face L336