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

CombinationID

show as:
view Lean formalization →

The inductive enumeration of nine implemented Option A combinations indexes the falsifier registry. Researchers auditing cross-domain theorems in Recognition Science cite it to assign empirical actions and deliverables to each case. The declaration introduces nine named constructors and derives decidable equality, string representation, and finite cardinality.

claimThe inductive type enumerating the implemented Option A combinations consists of nine cases: cognitive tensor, planet strata, oncology tensor, quantum molecular depth, attention tensor, Erikson reverse, universal response, Miller span, and regulatory ceiling.

background

The Option A Falsifier Registry maintains a finite pairing of cross-domain theorems with empirical test classes. This attachment prevents the cross-domain work from drifting into unfalsifiable numerology. The module carries zero sorry or axiom statements.

proof idea

Inductive definition that introduces nine constructors for the combinations and derives DecidableEq, Repr, and Fintype instances.

why it matters in Recognition Science

This enumeration anchors the empirical layer of the Option A registry. It supplies the domain for analysisAction and deliverableFor, which map each case to concrete actions such as fitFactorModel for oncology tensor and deliverables such as oncologyFactorModelNotebook. The structure supports theorems including hasAnalysisAction_all and EmpiricalActionPlanCert that certify completeness of the first-pass schedule. It directly implements the module goal of keeping falsifiers attached to the Lean theorem bundle.

scope and limits

formal statement (Lean)

  19inductive CombinationID where
  20  | c1CognitiveTensor
  21  | c2PlanetStrata
  22  | c3OncologyTensor
  23  | c4QuantumMolecularDepth
  24  | c5AttentionTensor
  25  | c6EriksonReverse
  26  | c7UniversalResponse
  27  | c8MillerSpan
  28  | c9RegulatoryCeiling
  29  deriving DecidableEq, Repr, Fintype
  30

used by (40)

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

… and 10 more