theorem proved term proof

`triple_card`

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

formal statement (Lean)

  67theorem triple_card {n : ℕ} (T : RSIndependentTriple n) :
  68    tripleProductCard T = n * n * n := by

proof body

Term-mode proof.

  69  unfold tripleProductCard
  70  rw [T.axis1.card_eq, T.axis2.card_eq, T.axis3.card_eq]
  71
  72/-- Cardinality of the disjoint sum of three same-size RS-independent axes. -/

depends on (15)

Lean names referenced from this declaration's body.

axis1 in IndisputableMonolith.Algebra.F2Power decl_use
axis2 in IndisputableMonolith.Algebra.F2Power decl_use
axis3 in IndisputableMonolith.Algebra.F2Power decl_use
card_eq in IndisputableMonolith.Algebra.F2Power decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
independent in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
independent in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
RSIndependentTriple in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
tripleProductCard in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use