Chemistry Nucleoside Structure From Config Dim

The counting of nucleosides

Nucleosides are the molecular subunits that make up the genetic material DNA and RNA. Each nucleoside pairs a nitrogenous base with a sugar. DNA uses four of them: adenine, thymine, cytosine, and guanine. RNA replaces thymine with uracil, giving a fifth. The standard complement structure pairs adenine with thymine (A-T) and cytosine with guanine (G-C), which is the basis of the double helix.

The five nucleosides form a small, complete set: adenine, thymine, cytosine, guanine, and uracil. In the Recognition Science framework, this set is modeled as a finite collection of exactly five distinct objects. The framework's machine-checked library proves this count directly: the theorem nucleosideCount establishes that the cardinality of the set is 5, by deciding each case.

DNA's four nucleosides have a structural pattern beyond their count. The framework models them as a subset of the five, excluding uracil. A second theorem, dna_nucleoside_count, proves that this subset has exactly 4 members. The interesting step follows: the framework proves that 4 equals 2 squared, written as 2². The theorem dna_equals_F2sq states that the DNA nucleoside count equals 2^2, which it proves by direct computation.

In Recognition Science, this 4 = 2² identity is not a coincidence. The framework interprets the DNA set as a two-dimensional binary space, often written F₂², where each of the two axes corresponds to a binary chemical distinction: purine versus pyrimidine, and keto versus amino. This gives a structural reason why DNA has four nucleosides rather than some other number: two independent binary choices yield exactly four combinations.

The module assembles these three facts into a single certificate. The structure NucleostructureCert bundles the five-total count, the four-DNA count, and the 2² identity into one object. The definition nucleostructureCert constructs this certificate from the three results. The Lean status reports 0 sorry and 0 axiom, meaning every step is checked by the kernel with no unproven assumptions.

What this establishes in plain language: the five nucleosides are exactly five, DNA uses exactly four of them, and those four correspond to two binary choices. The framework's contribution is not new biology; it is a formal, machine-checked statement of a known counting fact, tying the number 4 to the structure 2². This gives a compact algebraic description of why DNA has four standard building blocks.

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

structure NucleostructureCert where
  five_total : Fintype.card Nucleoside = 5
  four_dna : DNANucleoside.card = 4
  f2_structure : DNANucleoside.card = 2 ^ 2

def nucleostructureCert : NucleostructureCert where
  five_total := nucleosideCount
  four_dna := dna_nucleoside_count
  f2_structure := dna_equals_F2sq

What this page does not claim

This module does not prove that DNA must have four nucleosides; it proves the count is 4 given the defined set. The framework does not derive the chemical properties of nucleosides from the count alone. No claim is made about the biological function of the complement pairing beyond the structural 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: