agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Are allotropes of carbon hydrocarbons?

Open ghost opened this issue 2 years ago ā€¢ 4 comments

There are certain molecules called allotropes of carbon which consist entirely of carbon atoms. Examples include carbon nanotubes and fullerines. https://en.wikipedia.org/wiki/Allotropes_of_carbon https://en.wikipedia.org/wiki/Carbon_nanotube https://en.wikipedia.org/wiki/Fullerene With the current definition of hydrocarbon, these molecules are hydrocarbons with zero hydrogen atoms.

But I'm not sure if the chemistry community would call allotropes of carbon 'hydrocarbons', common usage seems to imply that there is at least one hydrogen atom in a hydrocarbon.

ghost avatar Jul 05 '22 16:07 ghost

I agree with you, hydrocarbons should probably have at least one hydrogen atom! Thank you again for your contribution!

EgbertRijke avatar Jul 05 '22 17:07 EgbertRijke

I believe this is already impossible. If we look at this confusing-perspective diagram of Cā‚†ā‚€ fullerene (from PubChem, but I'll take full blame for the hand-drawn highlighting), we see that the highlighted carbon has 4 incident edges.

image

But this isn't allowed:

(c c' : vertex-Undirected-Graph-š”½ G) ā†’ leq-ā„•
  (number-of-elements-is-finite (is-finite-type-š”½ (pr2 G (standard-unordered-pair c c'))))
  3)

Translating, in the type of hydrocarbons, each carbon (vertex in the underlying graph) can have at most three carbon-carbon bonds. This excludes every allotrope: they all have every carbon making 4 carbon-carbon bonds!

plt-amy avatar Jul 05 '22 22:07 plt-amy

The condition you mention here only excludes quadruple bonds between two carbon atoms in the molecule.

EgbertRijke avatar Jul 06 '22 12:07 EgbertRijke

According to Egbert Rijke in https://github.com/UniMath/agda-unimath/issues/234#issuecomment-1176187175 requiring the molecule to have at least one hydrogen atom implies that there are no quadruple bonds between two carbon atoms in the molecule, because the graph is connected.

madeleinebirchfield avatar Jul 06 '22 13:07 madeleinebirchfield