pith. machine review for the scientific record. sign in
theorem proved term proof high

fortyfive_is_gap

show as:
view Lean formalization →

The natural number 45 is identified with the gap45 parameter inside the Recognition Science cardinality spectrum. Cross-domain analyses cite the equality when confirming that 45 belongs to the structured list generated from cube primitives and configDim 5. The proof reduces to a single reflexivity step on the definition of gap45.

claim$45 = g_{45}$ where $g_{45}$ denotes the gap parameter in the RS cardinality spectrum.

background

The module C21 collects witnesses that RS cardinalities form the spectrum {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, …}. Each entry decomposes via multiplication, summation, or powers of the generators {2, 3}, the five-dimensional configDim, and the gap45 term. The local setting is the structural claim that these numbers are not arbitrary but arise directly from the RS stack.

proof idea

The proof is a one-line reflexivity step that matches the numeral 45 to the definition of gap45.

why it matters in Recognition Science

The equality anchors 45 inside the spectrum and thereby supports the module claim that every listed cardinality admits a decomposition into RS primitives. It fills the concrete witness slot for gap45 in the cross-domain cardinality spectrum C21.

scope and limits

formal statement (Lean)

  73theorem fortyfive_is_gap : (45 : ℕ) = gap45 := rfl

proof body

Term-mode proof.

  74
  75/-- 64 = 2⁶ = 8·8. -/