theorem proved term proof

`molecularQuantumStateClasses_25`

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

formal statement (Lean)

  29theorem molecularQuantumStateClasses_25 :
  30    molecularQuantumStateClasses = 25 := by

Term-mode proof.

  31  unfold molecularQuantumStateClasses
  32  rw [molecularEnergyCount, quantumGateTypeCount]
  33

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

molecularQuantumStateClasses_le_2pow5 in IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 decl_use
quantumMolecularDepthCert in IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 decl_use
twoPowerFour_lt_stateClasses in IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 decl_use

Lean names referenced from this declaration's body.

molecularEnergyCount in IndisputableMonolith.Physics.MolecularPhysicsFromRS decl_use
quantumGateTypeCount in IndisputableMonolith.Physics.QuantumComputingDepthFromRS decl_use
molecularQuantumStateClasses in IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 decl_use