Encyclopedia Chemistry Chemistry Nucleoside Structure From Config Dim Dna Nucleoside Count

ARTICLE 3 claims 2 theorems 1 open

Chemistry Nucleoside Structure From Config Dim Dna Nucleoside Count

DNA uses four nucleosides, but the framework's declaration is a count, not a chemical law.

Verify this page

The nucleoside count

DNA is built from four nucleoside units: adenine, thymine, cytosine, and guanine, usually written A, T, C, G. RNA replaces thymine with uracil, giving five canonical nucleosides in total. The declaration dna_nucleoside_count in the Recognition Science library states that the set of DNA nucleosides has exactly four members. It proves this by direct computation: the set is defined as containing those four named units and nothing else, so the cardinality is 4 by inspection.

The same library also proves that 4 equals 2 squared, written as 2^2, and connects this to a binary structure with two axes: purine versus pyrimidine, and keto versus amino. This is a formal observation about the counting, not a claim about biochemistry. The result does not say why DNA uses four nucleosides, does not derive the genetic code, and does not explain base pairing. It merely records that the finite set of DNA nucleosides has size four, and that this size matches 2^2.

In Recognition Science, the framework models recognition, a discrete record of events, and uses such counts as structural markers. Here the marker is the number 4, which the framework associates with a two-dimensional binary space. The declaration is a theorem in the machine-checked library of formal theorems, meaning the count is verified by the proof checker. It is not an empirical measurement from a laboratory, and it does not depend on any experimental data.

The honest scope is narrow. The declaration establishes a cardinality fact about a defined set. It does not claim that the set definition is biologically forced, that the binary axes are the reason for the count, or that the framework explains the origin of DNA's chemistry. Those are separate questions, some open, some outside the framework's current reach. What the declaration gives is a precise, checked statement: the DNA nucleoside set has four elements, and four is 2 squared.

THEOREM dna_nucleoside_count · IndisputableMonolith/Chemistry/NucleosideStructureFromConfigDim.lean
dna_nucleoside_count · IndisputableMonolith/Chemistry/NucleosideStructureFromConfigDim.lean:30 
theorem dna_nucleoside_count : DNANucleoside.card = 4 := by decide
THEOREM dna_equals_F2sq · IndisputableMonolith/Chemistry/NucleosideStructureFromConfigDim.lean
dna_equals_F2sq · IndisputableMonolith/Chemistry/NucleosideStructureFromConfigDim.lean:32 
/-- 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 claim that DNA's nucleoside count is biologically necessary or chemically derived. It does not claim that the binary axes (purine/pyrimidine, keto/amino) cause the count. It does not claim any empirical measurement of nucleosides.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND