pith. machine review for the scientific record. sign in
def definition def or abbrev high

abstractAlgebraCert

show as:
view Lean formalization →

The definition assembles three facts about the recognition lattice Q₃ into the AbstractAlgebraCert record: exactly five algebraic structures exist on it, its cardinality is 8, and its exponent is 2. A researcher tracing algebraic consequences from the Recognition Science forcing chain would cite this bundle to access the properties together. The construction is a direct record literal that assigns the three upstream theorems to the corresponding fields.

claimLet $Q_3$ be the recognition lattice. The certificate asserts that the number of algebraic structures on $Q_3$ equals 5, that $|Q_3|=8$, and that the exponent of $Q_3$ equals 2.

background

The module shows that the recognition lattice $Q_3$, identified with the abelian group $(ℤ/2ℤ)^3$, carries natural algebraic structure. From the Recognition Science framework, $|Q_3|=2^3$ matches the spatial dimension $D=3$, while the five structures (group, ring, field, module, algebra) match configDim $D=5$. The upstream theorem algebraicStructureCount establishes the structure count by decision. The theorem q3Size_eq_8 fixes the cardinality at 8 by decision. The theorem q3Exponent_eq_2 fixes the exponent at 2 by reflexivity.

proof idea

The definition is a direct record construction. It populates the five_structures field with algebraicStructureCount, the q3_size_8 field with q3Size_eq_8, and the q3_exp_2 field with q3Exponent_eq_2.

why it matters in Recognition Science

This definition packages the algebraic properties of $Q_3$ that follow from the eight-tick octave (T7) and the emergence of $D=3$ (T8) in the forcing chain. It supplies a single handle for the cardinality, exponent, and structure count that later derivations of abstract algebra from the Recognition Composition Law can reference. No downstream uses appear yet, so integration into proofs of physical constants or the phi-ladder remains open.

scope and limits

formal statement (Lean)

  41def abstractAlgebraCert : AbstractAlgebraCert where
  42  five_structures := algebraicStructureCount

proof body

Definition body.

  43  q3_size_8 := q3Size_eq_8
  44  q3_exp_2 := q3Exponent_eq_2
  45
  46end IndisputableMonolith.Mathematics.AbstractAlgebraFromRS

depends on (4)

Lean names referenced from this declaration's body.