theorem proved term proof

`eta_B_rung_from_chirality_eq`

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

formal statement (Lean)

  72theorem eta_B_rung_from_chirality_eq : eta_B_rung_from_chirality = -44 := by

proof body

Term-mode proof.

  73  unfold eta_B_rung_from_chirality bitFlipCount0 torsionGap01
  74  decide
  75
  76/-- Witness C (fermionic-DOF doubling): `A − fermionicDOF / 2`. -/

used by (3)

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

etaBExactRungCert in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
witnesses_AB_agree in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
witnesses_BC_agree in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use

depends on (7)

Lean names referenced from this declaration's body.

bitFlipCount0 in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
eta_B_rung_from_chirality in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
fermionicDOF in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
torsionGap01 in IndisputableMonolith.Cosmology.EtaBExactRungDerivation decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use