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

QFTTechnique

show as:
view Lean formalization →

QFTTechnique defines an inductive type whose five constructors enumerate the canonical methods of quantum field theory. A physicist deriving QFT from Recognition Science cites it to fix the configuration dimension at five. The definition directly supplies the Fintype instance whose cardinality is settled by a downstream decision procedure.

claimLet the set of quantum field theory techniques be the finite collection containing perturbation theory, renormalization, the path-integral formalism, Feynman diagrams, and lattice regularization, equipped with decidable equality and finite cardinality.

background

In the Recognition Science treatment of quantum field theory the vacuum is identified with the J-cost zero ground state. Renormalization group flow is reinterpreted as evolution of the recognition scale. The module states that five canonical techniques exhaust the configuration dimension, which is thereby fixed at five, and supplies the numerical target for the inverse fine-structure constant inside the interval (137.030, 137.039).

proof idea

The declaration is an inductive definition that introduces the five listed constructors and derives the DecidableEq, Repr, BEq and Fintype instances in a single step. No external lemmas are invoked; the finite cardinality follows immediately from the enumeration.

why it matters in Recognition Science

The definition supplies the five sectors required by the QFTDepthCert structure and the qftTechniqueCount theorem, which confirms that the cardinality equals five. It realizes the claim that the QFT vacuum comprises five distinct sectors drawn from the RS DFT-8 structure. The construction anchors the link between the Recognition Composition Law and standard QFT methods while the alpha band supplies the concrete numerical check.

scope and limits

formal statement (Lean)

  23inductive QFTTechnique where
  24  | perturbationTheory | renormalization | pathIntegral
  25  | feynmanDiagrams | latticeQFT
  26  deriving DecidableEq, Repr, BEq, Fintype
  27

used by (2)

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