agda-unimath
agda-unimath copied to clipboard
Are allotropes of carbon hydrocarbons?
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.
I agree with you, hydrocarbons should probably have at least one hydrogen atom! Thank you again for your contribution!
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.
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 hydrocarbon
s, 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!
The condition you mention here only excludes quadruple bonds between two carbon atoms in the molecule.
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.