theorem proved term proof

`two_cube_equicardinal`

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

formal statement (Lean)

  60theorem two_cube_equicardinal
  61    {A B : Type} [Fintype A] [Fintype B]
  62    (hA : HasTwoCubeCount A) (hB : HasTwoCubeCount B) :
  63    Fintype.card A = Fintype.card B := by

proof body

Term-mode proof.

  64  rw [hA, hB]
  65
  66/-- A 2³ cube squared: 64 = 2^6 (the six faces squared? No, 2^(2·3) — the
  67    product of two cube-8 structures). -/

used by (3)

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

dft_q3_equicardinal in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use
pauli_tick_equicardinal in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use
twoCubeUniversalityCert in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
HasTwoCubeCount in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use