module module

`IndisputableMonolith.Gravity.Track1BCPhysicalResidual`

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 (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.D2ScopingAudit module_import
IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import
IndisputableMonolith.Gravity.Track1BCStructural module_import

declarations in this module (69)

theorem physicalReggeEHFiniteProbeResidualTarget L41
def PhysicalReggeEHManifoldIntegralRemainingTarget L78
theorem physicalReggeEHFullRegge_tendsto_continuumIntegral_of_localCorrespondence L90
theorem physicalReggeEHUpgrade_reduces_to_manifoldIntegralTarget L113
theorem physicalReggeEHUpgrade_beyond_flatStructuralWitness L125
def PhysicalReggeEHFiniteProbeResidualConclusion L162
theorem physicalReggeEHFiniteProbeResidualConclusion_of_localCorrespondence L194
structure PhysicalReggeEHBianchiInterface L205
theorem physicalReggeEHBianchiInterface_of_localCorrespondence L224
def PhysicalReggeEHConcreteSliceLimitWeightTarget L247
theorem physicalReggeEHConcreteSliceLimitWeightTarget_holds L266
def PhysicalReggeEHConcreteRefinementFamilySliceTarget L288
theorem physicalReggeEHConcreteRefinementFamilySliceTarget_holds L295
def PhysicalReggeEHConcreteProductFilterTarget L312
theorem physicalReggeEHConcreteProductFilterTarget_holds L322
def PhysicalReggeEHConcreteDiagonalTarget L332
theorem physicalReggeEHConcreteDiagonalTarget_holds L345
structure PhysicalReggeEHConcreteRefinementFamilyTargetCert L359
def physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount L404
theorem physicalReggeEHConcreteRefinementFamilyTargetCertProjectionCount_eq_three L406
theorem physicalReggeEH_concrete_refinement_family_target_one_statement L414
theorem physicalReggeEH_concrete_refinement_family_target_one_statement_sliceTargets L426
theorem physicalReggeEH_concrete_refinement_family_target_one_statement_productTarget L434
theorem physicalReggeEH_concrete_refinement_family_target_one_statement_certInhabited L442
def physicalReggeEHConcreteRefinementFamilyOneStatementProjectionCount L451
theorem physicalReggeEHConcreteRefinementFamilyOneStatementProjectionCount_eq_three L453
theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement L460
theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement_sliceTarget L470
theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement_productTarget L478
theorem physicalReggeEH_concrete_varying_cardinality_product_filter_data_one_statement_certInhabited L486
def physicalReggeEHConcreteVaryingCardinalityProductFilterOneStatementProjectionCount L497
theorem physicalReggeEHConcreteVaryingCardinalityProductFilterOneStatementProjectionCount_eq_three L500
def PhysicalReggeEHFiniteProductResidualEstimateTarget L506
theorem physicalReggeEHFiniteProductResidualEstimateTarget_holds L516
def physicalReggeEHFiniteProductResidualEstimateProjectionCount L526
theorem physicalReggeEHFiniteProductResidualEstimateProjectionCount_eq_one L528
def PhysicalReggeEHContinuumNormalizationFromResidualTarget L534
theorem physicalReggeEHContinuumNormalizationFromResidualTarget_holds L546
theorem physicalReggeEHContinuumNormalizationFromResidualTarget_apply L559
def physicalReggeEHContinuumNormalizationFromResidualProjectionCount L574
theorem physicalReggeEHContinuumNormalizationFromResidualProjectionCount_eq_two L576
def physicalReggeEHContinuumMasterProp L585
theorem physicalReggeEHContinuumMasterProp_holds L591
def physicalSchlafliBianchiMasterProp L599
theorem physicalSchlafliBianchiMasterProp_holds L603
def physicalReggeEHContinuumAndBianchiWitness L609
theorem physicalReggeEHContinuumAndBianchiWitness_reggeClause L621
theorem physicalReggeEHContinuumAndBianchiWitness_reggeHolds L630
theorem physicalReggeEHContinuumAndBianchiWitness_bianchiClause L639
theorem physicalReggeEHContinuumAndBianchiWitness_bianchiHolds L648
structure PhysicalReggeEHD2MasterWitnessCert L657
def physicalReggeEHD2MasterWitnessCert L669
theorem physicalReggeEHD2MasterWitnessCert_witness_eq L680
theorem physicalReggeEHD2MasterWitnessCert_reggeClause L689
theorem physicalReggeEHD2MasterWitnessCert_bianchiClause L699
def physicalReggeEHD2MasterWitnessProjectionCount L709
theorem physicalReggeEHD2MasterWitnessProjectionCount_eq_seven L711
theorem physicalReggeEHD2MasterWitnessCert_inhabited L714
theorem physicalReggeEHD2_master_witness_one_statement L722
theorem physicalReggeEHD2_master_witness_one_statement_witnessInhabited L735
theorem physicalReggeEHD2_master_witness_one_statement_reggeEH L744
theorem physicalReggeEHD2_master_witness_one_statement_bianchi L753
def physicalReggeEHD2MasterWitnessOneStatementProjectionCount L762
theorem physicalReggeEHD2MasterWitnessOneStatementProjectionCount_eq_three L764
theorem physicalReggeEH_concrete_single_slice_product_filter_data_one_statement L772
theorem physicalReggeEH_concrete_single_slice_product_filter_data_one_statement_sliceTarget L787
theorem physicalReggeEH_concrete_single_slice_product_filter_data_one_statement_productTarget L798
def physicalReggeEHConcreteSingleSliceProductFilterOneStatementProjectionCount L809
theorem physicalReggeEHConcreteSingleSliceProductFilterOneStatementProjectionCount_eq_two L811