theorem proved term proof

`Q3_aut_order_eq`

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

formal statement (Lean)

  75theorem Q3_aut_order_eq : Q3_aut_order = Nat.factorial Q3_degree * 2 ^ Q3_degree := by

proof body

Term-mode proof.

  76  unfold Q3_aut_order Q3_degree; native_decide
  77
  78/-- The face-pair count: 2D² = 18 for D = 3.
  79    This is the structural number that appears in the η₂ correction. -/

depends on (11)

Lean names referenced from this declaration's body.

Q3_aut_order in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
Q3_aut_order in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
Q3_aut_order in IndisputableMonolith.Physics.CubeSpectrum decl_use
Q3_degree in IndisputableMonolith.Physics.CubeSpectrum decl_use