Chemistry Nucleoside Structure From Config Dim Nucleoside

The five nucleosides

Nucleosides are the molecular subunits that, when linked into chains, form the genetic material DNA and RNA. DNA uses four of them: adenine, thymine, cytosine, and guanine. RNA replaces thymine with uracil, making five canonical nucleoside types in total. The Recognition Science declaration Nucleoside, a discrete record of these five molecular building blocks, encodes exactly this familiar biological fact as a formal object.

The declaration defines the five nucleosides as distinct cases: adenine, thymine, cytosine, guanine, and uracil. A machine-checked theorem proves that the count is five. A separate definition collects the four DNA nucleosides, and another theorem proves that this DNA set has cardinality four. A further theorem shows that four equals two squared, written 4 = 2². This arithmetic identity is the entire mathematical content of the DNA structure claim.

The framework's library, a machine-checked collection of formal theorems, bundles these facts into a certificate structure. The certificate holds three statements: the total is five, the DNA subset is four, and the DNA subset size equals two squared. Each statement is proved by direct computation, meaning the Lean kernel checked the arithmetic by reducing the definitions. The certificate itself is a definition that assembles the three proofs, not a new theorem.

The biological significance is the base-pair complement rule. Adenine pairs with thymine, and cytosine pairs with guanine, which is why the four DNA nucleosides form two complementary pairs. The framework notes that these four can be seen as two binary axes: purine versus pyrimidine, and keto versus amino. This binary view is a modeling choice, not a proved biological law.

What the declaration does not claim is equally clear. It does not claim that nucleosides cause genetics, that the binary structure explains base pairing, or that the number five has any special physical necessity. The proofs establish counting facts about a defined list, nothing more. The biological reality of DNA and RNA stands independently of this formal exercise.

theorem nucleosideCount : Fintype.card Nucleoside = 5 := by decide

theorem dna_nucleoside_count : DNANucleoside.card = 4 := by decide

/-- 4 = 2² (F₂² at D=2). -/
theorem dna_equals_F2sq : DNANucleoside.card = 2 ^ 2 := by decide

What this page does not claim

The declaration does not prove that nucleosides are the building blocks of heredity. The binary structure does not explain why adenine pairs specifically with thymine. The number five is not derived from the framework's forcing chain; it is an observed biological count.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/NucleosideStructureFromConfigDim.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: