theorem proved term proof

`D5_counterfactual_rung`

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

formal statement (Lean)

 132theorem D5_counterfactual_rung : eta_B_rung_from_dimension 5 = -174 := by

Term-mode proof.

 133  unfold eta_B_rung_from_dimension integrationGap parityCount configDim A
 134  decide
 135
 136/-! ## Master certificate -/
 137

Lean names referenced from this declaration's body.

configDim in IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS decl_use
eta_B_rung_from_dimension in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
configDim in IndisputableMonolith.Foundation.IntegrationGap decl_use
integrationGap in IndisputableMonolith.Foundation.IntegrationGap decl_use
parityCount in IndisputableMonolith.Foundation.IntegrationGap decl_use
configDim in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use