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

gap45_eq

show as:
view Lean formalization →

The equality gap45 = 45 holds by definition in the RS-coupled axes setup. Researchers in cross-domain cardinality spectra and dark matter mass ratios cite this to fix the numerical value of the gap parameter derived from spatial and configuration dimensions. The proof is a one-line reflexivity confirming the definition matches the integer 45.

claimIn the RS-coupled axes construction the gap parameter satisfies $gap_{45} = 45$.

background

The RS-Coupled Axes module supplies infrastructure for cross-domain combination theorems. Its central convention is that two finite axes of equal cardinality count as independent only when they carry distinct recognition primitives. The gap45 parameter is imported from the cardinality spectrum, where an upstream result states gap45 = D_spatial² × D_config; a second upstream result already records the numerical value 45.

proof idea

The proof is a one-line reflexivity that applies rfl directly to the definition of gap45.

why it matters in Recognition Science

This equality supplies the concrete value required by the cardinality spectrum certificate (via gap_as_D) and by the dark matter mass certificate (via gap45_val). It also populates the gap45_eq field inside the style succession certificate. The result aligns with the framework's assignment of D = 3 spatial dimensions and the eight-tick octave, since 3² × 5 yields exactly 45, thereby closing the numerical anchor for downstream applications in art history and physics.

scope and limits

formal statement (Lean)

  83theorem gap45_eq : gap45 = 45 := rfl

proof body

Term-mode proof.

  84
  85end RSCoupledAxis
  86end Foundation
  87end IndisputableMonolith

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.