IndisputableMonolith.Gravity.ReggeComponentTheorem3DProof

declarations in this module (19)

• structure IndependentDualWeights L28
• def edgePairIncidenceWeight L35
• def vertexPairHingeWeight L47
• theorem edgePairIncidenceWeight_symm L52
• theorem vertexPairHingeWeight_symm L73
• theorem vertexPairHingeWeight_nonneg L84
• def independentDualWeightsOfIncidence L98
• def independentDualWeightsOfConsistent L107
• def canonicalWeakFieldDataOfIncidence L115
• theorem canonicalWeakFieldData_bilinearCoefficient L122
• theorem canonicalWeakFieldData_rowSum L131
• theorem canonicalWeakFieldData_offDiag_component_match L138
• structure ConcreteComponentComparison L147
• def FinalReggeComponentTarget L155
• def concreteComponentComparisonOfIncidence L160
• theorem finalReggeComponentTarget L170
• def genuineComponentPackage_of_concrete L175
• theorem genuine_component_package_of_final L186
• theorem genuine_component_dirichlet_reduction_from_final L196